Comment by Someone
11 days ago
> The implemented Rust semantics are not sound, as evidenced by this issue. We need to find (or adjust) sound semantics.
You’re ignoring the possibility that Rust semantics are sound, and the implementation doesn’t fully implement them. In that case, we do not have to find sound semantics.
That, I think, by far is the most likely option.
Reason: I’ve not seen a single comment claiming the example should compile, and zillions (implicitly) acknowledging this is not what Rust should do.
I explicitly did not ignore the option that there are possible sound semantics:
> but not necessarily for this one specifically
> Maybe, maybe not.
But "the Rust semantics" are not defined, formally. The closest we have is what Rust implements currently, and that was shown here to not be sound. Other than that, we maybe have vague ideas in the brains of some T-types members, which are not detailed enough to determine soundness (source: those type system people want to formalize the semantics so they will be).
And for the record, we know of other soundness issues where the likely resolution path will involve rejecting valid programs we accept now, and the only question is how many.
"the Rust semantics" are defined informally as sound. Anything that the implementation accepts that is unsound is a bug. We might never be able to prove the rust implementation, and may forever find loop holes, but informally it is sound and that is the intent.
There is no such thing as "informally sound". Soundness is a mathematical property and needs to be proven mathematically. For that, you first need a mathematical definition.