> With a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check th

> With a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. This approach would only be able to verify a particular compilation result as safe. If you want to verify that it will always be safe, you need to be comparing against the behavior of future compilers, which requires some kind of contract about their behavior. “Formal semantics” is the technical term for that contract.