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.
Re:A Sad Day for Rust
by fluffything on Monday January 20, 2020 @10:01AM
(#22099237)
> 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.
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.