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)
>> 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)