> These are classic proof of correctness areas. It's fairly straightforward to state the conditions that have to be proven, and usually not that hard to prove them.

You're right, but current Rust cannot express logical preconditions in code, much less compiler-checkable proofs. Many groups are working on this via a variety of approaches, but it will take some time before there's a common standard for expressing these things as part of the Rust language itself.