4 ms·

Are you seriously suggesting rusts memory safety promises are ok if they simply 'kind of probably protect you from memory corruption'? /me shakes head. Time f

• Manishearth 11y ago
  It's not practical to formally verify everything. We'd get nothing done if that was the case. Rust's memory safety promises can be reasoned about clearly without formal verification (which is an arduous process requiring a team of researchers -- basically what RustBelt is doing). This is enough to be convinced that Rust is protecting you from memory corruption. Formal correctness proofs are valuable, but not necessary to ship software. Also, as others have mentioned, Rust is a strict plus over C++ in formal verification as well since once you've verified a module containing unsafe code, you can forget that it contains unsafe code and use it wherever, and modules with safe code can be used without verification. Once verified, Vec<T> is safe to use however you want as long as it's not used in an unsafe block (if it is, just verify that block or module depending on the context).