On Mon, 28 Nov 2005 10:02:19 +0100, Sybren Stuvel wrote: > Duncan Booth enlightened us with: >> I would have thought that no matter how elaborate the checking it is >> guaranteed there exist programs which are correct but your verifier >> cannot prove that they are. > > Yep, that's correct. I thought the argument was similar to the proof > that no program (read: Turing machine) can determine whether a program > will terminate or not.
No, that is not right -- it is easy to create a program to determine whether *some* programs will terminate, but it is impossible to create a program which will determine whether *all* programs will terminate. -- Steven. -- http://mail.python.org/mailman/listinfo/python-list
