Crucially, unsafe is also about the social contract. Rust's compiler can't tell whether you wrote a safety rationale adequately explaining why this use of unsafe was appropriate, only other members of the community can decide that. Rust's compiler doesn't prefer an equally fast safe way to do a thing over the unsafe way, but the community does. You could imagine a language with exactly the same technical features but a different community, where unsafe use is rife and fewer of the benefits accrue.

One use of "unsafe" that was not mentioned by Nora but is important for the embedded community in particular is the use of "unsafe" to flag things which from the point of view of Rust itself are fine, but are dangerous enough to be worth having a human programmer directed away from them unless they know what they're doing. From Rust's point of view, "HellPortal::unchecked_open()" is safe, it's thread-safe, it's memory safe... but it will summon demons that could destroy mankind if the warding field isn't up, so, that might need an "unsafe" marker and we can write a checked version which verifies that the warding is up and the stand-by wizard is available to close the portal before we actually open it, the checked one will be safe.

This is a complete misuse of the unsafe as language concept in high integrity computing.

Real formal verification is clearly a step up from rust's meaning of "safe", but I don't think it's wrong to try to add another rung to the verification ladder at a different height. Verification technologies have a lot of space to improve in the UX department, here Rust trades off a some verification guarantees for a practical system that is still meaningful.

Real formal verification in Rust is basically waiting for a proper formal model of Rust semantics (including semantics of "unsafe"). This is one of the most unappreciated things about Rust's future potential, AIUI; the only language in common use that supports both systems-level programming and formal proof is ATS.

Eh. You can write, and people have written, formal proofs about C code too. In fact, the difference between Rust and C in terms of safety isn't very large if you have an infinite budget to put toward proving all the code that you write correct.

The safety benefits of Rust appear when you aren't willing to formally prove all the code you write correct. That's because you only have to prove the unsafe code, plus the memory model, correct in order to guarantee memory safety for the entire program. This is less burdensome than in C, where to do the same you have to prove correctness properties about the specific code that makes up the whole program. Rust makes it easier to prove certain properties about the program (far easier in the case of memory safety), but it was always possible.

I’m doing my PhD on the formal verification of Rust, and while you’re right that safe code provides a lot of informal advantages it also dramatically simplified form reasoning.

In particular, the dirty secret of C verifiers is that they don’t handle pointers all that well. Either you find yourself doing a lot of manual proof work or you have to dramatically simplify the memory model.

In contrast, when verifying safe Rust, the rules of the borrow checker allow us to dramatically simplify the verification work. All of a sudden verifying a manual memory program with pointers (borrows) becomes as simple as verifying a basic imperative language. I’ve been working on a tool: https://github.com/xldenis/creusot to put this into practice

On the other hand, the moment you dive into unsafe, all bets are off and you find yourself wading through the marshes of (weak) memory models with your favorite CSL as your only friend.

Note that there are other tools trying to deal with formal statements about Rust programs. AIUI, Rust developers are working on forming a proper team or working group for pursuing these issues. We might get a RFC-standardized way of expressing formal/logical conditions about Rust code, which would be a meaningful first step towards supporting proof-carrying code directly within Rust.