logoalt Hacker News

i2talics • today at 4:52 PM • 0 replies • view on HN

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.