We don't need to verify every single occurrence of unsafe, but whenever unsafe is necessary I feel the lack of some other guarantee holding our back.
Having optional small-scale(!) verification in Rust would be awesome.
Using other theorem provers has the same problems as when one tries to establish tools for checking memory safety in C: it isn't the default, just an addon.
In my eyes, there is a scale of verification-readiness in which Rust can position itself. The least ready would be having it completely separate and done by other tools in other files, the most ready would be having syntax for it in the language, having it in the same files, and checked by the standard compiler.
I think every bit of verification-readiness Rust has by default will have a strong effect that we can't achieve through other means.
Maybe, some things don't impact those not interested in verification. Say, have next to 'safe' and 'unsafe' also the 'verified' environment that also contains proof language as a core part of Rust. That way all ordinary code is still valid and everyody is free to use Rust without verification in mind.
Any ideas what could be done to make Rust verification-readier?
However, I honestly feel that the Rust language itself isn't really the right language to be doing these kinds of proofs in. I think that the right language to do the actual formal verification in is likely to be something closer to Coq. Whoever undertakes this effort would probably use an automated theorem prover to prove the unsafe Rust code correct, like was done for seL4 using Isabelle.
You can think of this setup as offering a sort of layered verification: once the small core of code (the unsafe code in the standard library and popular crates, say) is proven correct, the type system and borrow checker effectively prove the rest to be memory- and thread-safe. In fact, that's what would make this system practical: most programmers wouldn't have to understand anything about the complexities of the theorem prover. They would get the benefit of verified memory- and thread-safety for free just by learning Rust.