Comment by remywang
9 hours ago
> 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
> How do you verify this compiler is correct?
I haven't yet. My main goal has been to find as many bugs as possible. While bugs could still slip through because my compiler is incorrect, I'm still finding a good number, so I think it's worth it.
Did you consider using an established Rust verification toolchain like Aeneas?
Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?
AFAICT, Aeneas only supports a safe subset of Rust. I needed something that could support all of Rust
> I think you at least need a formal semantics for both C
https://en.wikipedia.org/wiki/CompCert
> formal semantics for both C and Rust in Lean, both sound like Herculean efforts
If we're doing Ancient Athens, then Platonic Methexis probably fits better.