[fluffything]

> And introducing the language of "safe" and "unsafe" isn't just descriptive, it's a value judgment.

`unsafe` is a PL term that refers to _soundness_. In Rust, an `unsafe { ... }` block is required to perform an `unsafe` operation, and it precisely means "The code in this block has been proven _sound_". If the code in the block turns out to be _unsound_, e.g., because the proof is incorrect, or non-existent, then the whole program is unsound, and there is nothing that can be said about the execution of such program (usually known as "the execution exhibits undefined behavior").

For example, the Rust compiler has a lint that requires you to write a soundness proof on every `unsafe { ... }` block, explaining why that is sound, and all changes to the compiler are gated on that.

In your own projects, you can obviously do whatever you want, but for any non-trivial amount of unsafe code, without a proof, you are basically just building castles in the air.

[rowanG077]

That's an interesting way too look at it. But that's not how it works in practice. Almost no one in industry is going to write proofs for their unsafe code. It didn't happen for C or C++ and it won't happen for Rust.

[dthul]

In Rust you at least know where to look at, whereas in C/C++ all code can be "unsafe". With that said, writing unsafe Rust is much easier to screw up than C/C++, since you have to uphold more invariants in unsafe Rust than in C to avoid UB (like never having two mutable references to the same thing at the same time. The very issue which was raised in the actix repository)

[fluffything]

This is how it works in practice for the Rust compiler for the Rust standard library, and for a lot of foundational crates in crates.io. (Pretty much every well reviewed crate in cargo crate review either does this, or does not contain any unsafe code at all).

We also have tools that change for this for very large projects (e.g. cargo-geiger), and tools that help you test your proofs (e.g. cargo-miri). For some unsafe components, there are also proofs in Coq, and the proof systems for Rust unsafe code are making a lot of progress in both defining the rules that unsafe code must uphold in the unsafe-code-guidelines and the Rust spec, as well as in providing example proofs and a standard library of theorems that you can reuse for your own proofs.

[rowanG077]

I didn't say it no one will do it. I said almost no one. The Rust compiler is about as far from a normal project as can be. I would like to see this changed but really I have never even seen a proof requirement when looking at Rust jobs. Not even once.

[fluffything]

> I would like to see this changed but really I have never even seen a proof requirement when looking at Rust jobs. Not even once.

?

Any B.Sc. in CS can do most of the unsafe proofs in a one liner. All crates I maintain require unsafe blocks to be commented with a proof, for most of them the proofs are trivial, and for all of them that weren't, the unsafe code was correct, and the correct one had a trivial proof.

[rowanG077]

It's fine that YOU do it. But how many unsafe blocks have a proof in the entire Rust ecosystem (read all crates). 5% maybe? I'm not sure what your point is that any B.Sc. in CS can do it.