Steven D'Aprano <[EMAIL PROTECTED]> writes: > 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.
Which means you can't create a verifier which will verify all programs. Is there a reason to believe that you can't have a verifier with three possible outcomes: Correct, Incorrect, and I don't know, and it is always correct in doing so? Note that "I don't know" could be "I ran longer than I think is reasonable and gave up trying." <mike -- Mike Meyer <[EMAIL PROTECTED]> http://www.mired.org/home/mwm/ Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information. -- http://mail.python.org/mailman/listinfo/python-list
