On: Verified Rust for low-level systems code

[samatman]

A trivial proof is still a proof.

There's nothing trivial about "const a: int = foo();" though. Compilers disprove the claim by contradiction all the time.