[bb88]

If you choose to go through the effort, Haskell can be shown to be provably correct -- that is in a mathematical sense of the term "prove" -- similar to Ada/SPARK.

https://stackoverflow.com/questions/4077970/can-haskell-func...

AIUI, similar work is being made to Rust to make it have similar provable properties.

[Iv]

Thing is, in Rust, you can't choose not to go through the effort. The borrow checker forces you to do so.