Comment by malisper

7 hours ago

> 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