Exactly! And yet Rust gets a reputation of safety: the boundary between safe and unsafe is formal, and that opens up huge possibilities for metrics, compliance, and targeted testing. That’s what I’d shoot for.
People say this a lot. But formal methods is really hard and really tedious. Especially if you can't write whatever you're trying to prove safe in safe rust, it's going to be even harder and more tedious.
To give perspective: CompCert (a C compiler with formally-proven semantics, arguably one of the largest formally-proven programs to date) has been developed for decades and still does not support all C99 features; it and sel4 (a formally-verified safe microkernel) are both single-core because proving properties in complex multicore interactions has basically not been done (sel4 actually does have a multicore implementation, but it's not yet formally verified).
Safety, performance, ease-of-use: pick two. If we really care about safety, the easiest solution for many is to just use a language like Java or Python where everything is boxed and checked and there is no truly unsafe code. Safe Rust strikes a really nice balance of being almost formally-proven safe, almost as performant as unsafe Rust/C++, and almost as easy to use as more general-purpose-languages (the extent of the third "almost" varies widely among developers).
