Comment by masklinn

> Note that Rust is not a theorem prover

Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.