Comment by afdbcreid
11 days ago
It does apply, of course (even if not to this case specifically). The implemented Rust semantics are not sound, as evidenced by this issue. We need to find (or adjust) sound semantics. Which, mathematically, is equivalent to designing Rust from scratch (ignoring things like RustBelt because they did not formalize the entire system). Due to Rice's theorem we know we need to give up some sound programs. Can we give up exactly the programs we already gave up for the previous Rust? Maybe, maybe not.
The tricky thing about formalization is that you usually have to reimplement the type checker into a proof assistant in order to do formal soundness proofs. It's not necessarily clear that this reimplementation is identical to the actual Rust compiler (in fact, you often have to massively simplify the type system to make the proofs tractable), so bugs in implementation can cause unsoundness without being related to fundamental flaws in the soundness of the type system.
Indeed. Proving the implementation will likely never be done, it's just way too hard. But proving Rust abstract semantics are sound will by itself be a major leap forward (RustBelt did that for a subset of Rust).
> 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.
1 reply →
It could be that I'm totally yapping bullshit, but the "designing from scratch" can vary depending which field of maths you're talking about. For instance, if we model the semantics as a series of composable functions, then you only have to scratch only the specific dependency tree of the functions. Basically everything can be reused with no wasted work, and the output space gets culled.
Which is why I said to ignore RustBelt. Because we don't have formal semantics today, we only have the actual implementation which is not composable.