return in loop for ?

[Steven D'Aprano]

On Mon, 28 Nov 2005 12:05:03 -0500, Mike Meyer wrote:

> 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. 

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.