Comment by est31

By similar i meant the strong and powerful type system that Rust has, plus its safety guarantees (iterator invalidation is a compiler error etc). That is in the end a proof system: you are proving to the compiler that you really don't mutate the buffer and you can't drop the T in &T, etc.

Of course the Rust language doesn't give you tools to prove that the program is bug-free or such. The proofs only extend to a basic set of properties, but there is a proof system in Rust.

As for other ML languages, they aren't really C/C++ competitors performance wise, Rust is.