4 ms·
> Surprisingly, correctly describing the set of programs that have undefined behavior in a formal manner is the hardest part of formalizing C. Isn't this undec
by JabavuAdams 11y ago
> Surprisingly, correctly describing the set of programs that have undefined behavior in a formal manner is the hardest part of formalizing C.
Isn't this undecidable?
- obastani 11y agoI think that statement is referring to simply defining "undefined behavior", not actually determining whether a given program has undefined behavior.
- mikeash 11y agoYes, but that doesn't mean you can't describe it. The halting problem is undecidable, but it's really easy to describe the set of programs that halt. I just described it right there! That quote is talking about defining the set, not determining whether a program is a member of the set (which is indeed impossible in the general case).