On Mon, 28 Nov 2005 12:05:03 -0500, Mike Meyer wrote: > 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.
I thought that's what I said originally *wink* > 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." That seems perfectly reasonable to me. I don't know about anyone else in this discussion, but I'm talking about *theoretical* source code verification of formal correctness. In *practice*, I don't know what the state of the art is, but I suspect it will be a long, long time before it is as easy as running "import mymodule; verify(mymodule)". -- Steven. -- http://mail.python.org/mailman/listinfo/python-list
