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