[5738] in cryptography@c2.net mail archive
Re: having source code for your CPU chip -- NOT
daemon@ATHENA.MIT.EDU (Eli Brandt)
Thu Sep 23 20:05:30 1999
Message-Id: <199909232239.PAA13902@blacklodge.c2.net>
To: crypto list <cryptography@c2.net>
Date: Thu, 23 Sep 1999 18:38:57 -0400 (EDT)
From: Eli Brandt <eli@v.gp.cs.cmu.edu>
In-Reply-To: <v04210100b40fe1e79b73@[24.218.56.100]> from "Arnold Reinhold" at Sep 23, 99 11:14:32 am
Reply-To: eli+@cs.cmu.edu
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
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 | eli+@cs.cmu.edu | http://www.cs.cmu.edu/~eli/
