return in loop for ?

[Steve Holden]

Steven D'Aprano wrote:
> On Thu, 24 Nov 2005 12:51:34 +0000, Duncan Booth wrote:
> 
> 
>>Steven D'Aprano wrote:
>>
>>
>>>>While outwardly they apear to offer a technique for making software
>>>>more reliable there are two shortcomings I'm leery of. First, no
>>>>verification program can verify itself; 
>>>
>>>That's not a problem if there exists a verification program A which
>>>can't verify itself but can verify program B, which in turn also can't
>>>verify itself but will verify program A.
>>>
>>
>>That is logically equivalent to the first case, so it doesn't get you 
>>anywhere. (Just combine A and B into a single program which invokes A 
>>unless the input is A when it invokes B instead.)
> 
> 
> Then there you go, there is a single program which can verify itself.
> 
> I think you are confabulating the impossibility of any program which can
> verify ALL programs (including itself) with the impossibility of a program
> verifying itself. Programs which operate on their own source code do not
> violate the Halting Problem. Neither do programs which verify some
> subset of the set of all possibly programs.
> 
> 
There seems to have been some misattribution in recent messages, since I 
believe it was *me* who raised doubts about a program verifying itself. 
This has nothing to do with the Halting Problem at all. A very simple 
possible verification program is one that outputs True for any input. 
This will also verify itself. Unfortunately its output will be invalid 
in that and many other cases.

I maintain that we cannot rely on any program's assertions about its own 
formal correctness.

regards
  Steve
-- 
Steve Holden       +44 150 684 7255  +1 800 494 3119
Holden Web LLC                     www.holdenweb.com
PyCon TX 2006                  www.python.org/pycon/