2 ms·

It seems like you're assuming the post is saying that you need formal verification to write safe Rust? I don't think that's the case. Note that the blog post i

It seems like you're assuming the post is saying that you need formal verification to write safe Rust? I don't think that's the case. Note that the blog post is explicitly in the context of formally verifying Rust and its stdlib. This is not something that's necessary for a "good enough" guarantee that stuff works and is safe. The conclusion you can make is that formally verifying Rust is just as hard as C++ (I'm not sure I agree with this either, but it's really irrelevant), but this doesn't make Rust a worthless language since formal verification is not what you care about for everyday safety guarantees. > If the burden of 'safety' is formal proof of the entire module, then you're (surely) no better off than using C++ and doing exactly the same thing. Well, formal verification is nice, but it's not necessary. Take the Vec<T> interface for example. There are a couple of unsafe methods in it, and the invariant "len is always a valid length". It's easy to check if len is being modified elsewhere. It's easy to reason about these invariants. And it's easy to reason that it upholds the invariants that Rust expects for safe functions. Formal verification is harder, but practical verification is easier since it's contained in a small surface area. On the other hand, there's no "containment of unsafety" in C++ and other languages and even practical verification can be hard especially when generics get in the way. > In other words, if your rust program has any module in any dependency that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a 'safe' function that has not be formally verified to be safe, and results in undefined behaviour despite being safe). "Potentially unsafe" for a very small probability. You don't need formal verification to be convinced that something is safe.

shadowmint 11y ago
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 for bed.
- 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).

shadowmint 11y ago

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 for bed.

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).