Comment by afdbcreid
11 days ago
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.