return in loop for ?

[Mike Meyer]

Steven D'Aprano <steve at REMOVETHIScyber.com.au> 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 <mwm at mired.org>			http://www.mired.org/home/mwm/
Independent WWW/Perforce/FreeBSD/Unix consultant, email for more information.