> 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? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts
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.
Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?
"Aeneas currently functionalizes a subset of safe Rust, and we are in the process of extending the functional model with reasoning based on separation logic to support unsafe code and concurrent code."
If we're doing Ancient Athens, then Platonic Methexis probably fits better.