Comment by wongarsu

There is a formally proven compiler for a large subset of C, so I don't see why formalizing (a large subset of) rust and making a formally proven compiler shouldn't be possible