Comment by remywang

> I wrote a compiler that can translate both Rust and C code into Lean

How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts