return in loop for ?

[Steven D'Aprano]

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.