Arnold Reinhold wrote:
> Perry, if you really believe that the question of whether a given
> lump of object code contains a Thompson Trap is formally undecidable
> I'd be interested in seeing a proof. Otherwise Herr Goedel has
> nothing to do with this.
That sure smells undecidable to me. Any non-trivial predicate P on
Turing machines (non-trivial meaning that both P and not-P are
non-empty) is undecidable by Rice's Theorem. There are technical
issues in encoding onto the tape all possible interactions with the
world -- the theorem doesn't apply if some inputs are deemed illegal
-- but, hey, it's all countably infinite; re-encode with the naturals.
The practical impact of this is not immediately apparent. All
non-trivial theorem-proving about programs is futile in this same
sense, but people do it, or try. They have a lot of difficulties less
arcane than running into the pathological cases constructed to prove
these undecidability theorems.
> Your argument reminds me of claims I always
> hear that nothing can be measured because of the Heisenberg
> Uncertainty principle.
I do feel your pain.
--
Eli Brandt | [EMAIL PROTECTED] | http://www.cs.cmu.edu/~eli/
