alt Hacker NewsRice's theorem does not apply. This is not about what the compiler does, it is your program. If your program is not sound then it is invalid Rust even if the compiler accepts it and it seems to do the right thing.
That said, I was sarcastic.
Replies
afdbcreid • today at 3:50 PM
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.
➕ show 3 replies
Terminological nitpick, but soundness is a property of an entire type system not of an individual program. A type system is sound if it only accepts valid programs. A program is valid if it never exhibits undefined behavior.
Rice's theorem implies that it's impossible to precisely distinguish valid and invalid programs just by looking at their source code. Thus Rust rejects some valid programs in order to be sound (e.g. "if false { None.unwrap_unchecked() }").
In the case of the bug report in OP, I don't think that there are many valid programs in practice that exploit this soundness issue, so fixing it just means rejecting more invalid programs.