The GP had a few misconceptions about Godel and halting problems and stuff, but one nitpick here: >> Practically, this means that there will never be a compile

The GP had a few misconceptions about Godel and halting problems and stuff, but one nitpick here: >> Practically, this means that there will never be a compiler that will tell you whether you program has a bug. > > TLA+ and other "external" systems can evaluate whether a program has a bug. The main TLA+ model checker is TLC. It's pretty easy to write a TLA+ spec with a bug that TLC can't find (ironically by exploiting unbound model spaces, which are the Does Not Halt of model checking)