return in loop for ?

[Steven D'Aprano]

On Mon, 28 Nov 2005 08:44:04 +0000, Duncan Booth wrote:

> Steven D'Aprano wrote:
> 
>> Since real source code verifiers make no such sweeping claims to
>> perfection (or at least if they do they are wrong to do so), there is
>> no such proof that they are impossible. By using more and more
>> elaborate checking algorithms, your verifier gets better at correctly
>> verifying source code -- but there is no guarantee that it will be
>> able to correctly verify every imaginable program.
>> 
> I'm sure you can make a stronger statement than your last one. Doesn't 
> Godel's incompleteness theorem apply? 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.

Yes, of course. By saying "no guarantee" I was guilty of understatement:
at the very least, we can guarantee that the verifier will *not* correctly
verify every possible program. (Which of course is no different from human
programmers.)

-- 
Steven.