So if I understand correctly, an unsafe fn(T) is correct if there exists ("union") some precondition stronger than T that makes the function correct? Great, I pick s := ∅, i.e., precondition False. This means all unsafe fn are trivially "semantically well-typed", which makes that claim rather useless.
I wasn't talking about having picked the wrong semantics for a particular type. I was talking having set up the entire structure of the semantics in such a way that we accidentally ruled out some things we meant to allow. This can happen easily, e.g., the original RustBelt would not have allowed GhostCell. The only way to fix this is a global change and re-checking all proofs -- in other words, a breaking change, Rust 2.0.
Mistakes have certainly been made, but I think it is fair to say that Rust's UB story never was nearly as bad as that of C. Miri did not exist from the start, but there were also no choices made that would make Miri impossible. (For example, in C, an infinite loop can be UB under some circumstances. That kind of UB is a very bad idea IMO and Rust never had it.) To be clear, I am not blaming C here; the very understanding of what UB even is changed during the lifetime of C, so some early choices have not aged well.