> the existence of unsafe Rust means that Rust as a whole isn't safe by construction
That's true, and it's a good reason to be very clear about when the Safe Rust subset is all that's been used. Unfortunately it's rare to hear written in Safe Rust, but that's how we ought to refer to code written purely in the safe subset. It should be a point of pride. (Corollary: making needlessly excessive use of Rust's unsafe features, should be a point of shame.)
> We also need to be careful about what we mean by "safe". Rust's definition of safety isn't exotic
Rust does a fine job of defining safety as they use it:
> If all you do is write Safe Rust, you will never have to worry about type-safety or memory-safety. You will never endure a dangling pointer, a use-after-free, or any other kind of Undefined Behavior. [0]
This total absence of undefined behaviour definition sounds about right to me. I think Safe Rust also guarantees against reading indeterminate data from an uninitialized variable, but by the total absence of undefined behaviour criterion, that's not strictly relevant to whether it's safe.
> it doesn't cover the gamut of all possible safety concerns.
Sure, but that's not really what safe language means.
> But to prove whether your unsafe code is, in fact, safe to use -- you're back to formal verification again, or (more typically) code reviews.
At the risk of sounding pedantic, code reviews do not prove anything about unsafe code, they only lower the odds of a defect making it through your process.
> You can (often) avoid the use of unsafe Rust altogether, but then you're using a subset of the language -- roughly like the case with MISRA C.
I'd flip that round though, as you generally shouldn't be using Rust's unsafe features. I'd rather say that in the rare case that you really need it, Rust offers additional unsafe features beyond the Safe Rust language.
Safe Rust is intended to have excellent ergonomics, very much unlike MISRA C. If Rust is doing its job, its unsafe features should seem like inline assembly in C. C programmers don't generally feel constrained by an absence of assembly code in their codebases, as that kind of code just isn't necessary very often.
(Also, MISRA C isn't a truly safe language, for what that's worth. C is not so easily tamed.)
[0] https://doc.rust-lang.org/nomicon/meet-safe-and-unsafe.html