One of the fundamental differences is that in Rust, you only have to prove correct every module that contains unsafe code, and the proof then automatically expa

One of the fundamental differences is that in Rust, you only have to prove correct every module that contains unsafe code, and the proof then automatically expands to your entire program. The experience in practice is that most module - the ones that are "higher up" in the stack of abstraction - do not need unsafe code, and hence they are automatically safe. If someone proves the Rust libstd correct, and you write a Rust program using only libstd that does not contain unsafe, then your code is guaranteed to be safe. If someone proves the C++ libstd correct, and you write a program using only the C++ libstd - you still have to prove your code correct. Rust provides safe encapsulation, C++ does not.