return in loop for ?

[Steven D'Aprano]

On Fri, 25 Nov 2005 08:36:48 +0000, Steve Holden wrote:

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

Fair enough.

> This has nothing to do with the Halting Problem at all. 

On the contrary, the Halting Problem is just a sub-set of the verification
problem. Failure to halt when it is meant to is just one possible way a
program can fail verification.

On the one hand, the Halting Problem is much simpler than the question of
proving formal correctness, since you aren't concerned whether your
program actually does what you want it to do, so long as it halts.

But on the other hand, the Halting Problem is so much harder that it
actually becomes impossible -- it insists on a single algorithm which is
capable of checking every imaginable input.

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.


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

No doubt. But slightly more complex verification programs may actually
analyse the source code of some arbitrary program, attempt to use formal
algebra and logic to prove correctness, returning True or False as
appropriate.

That program itself may have been painstakingly proven correct by teams of
computer scientists, logicians and mathematicians, after which the
correctness of its results are as certain as any computer program can be.
That is the program we should be using, not your example.

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

There are two ways of understanding that statement.

If all you mean to say is "We cannot rely on any program's assertions
about any other programs formal correctness, including its own", then I
can't dispute that -- I don't know how well formal correctness checking
programs are. It is possibly, I suppose, that the state of the art merely
returns True regardless of the input, although I imagine a more realistic
estimate is that they would at least call something like pylint to check
for syntax errors, and return False if they find any.

But if you mean to say "While we can rely on the quality of correctness
checkers in general, but not when they run on their own source code" then
I think you are utterly mistaken to assume that there is some magic
quality of a verification program's own source code that prevents the
verification program working correctly on itself.

And that was my point: formal correctness checking programs will be as
good as testing themselves as they are at testing other programs. If you
trust them to check other programs, you have no reason not to trust them
to check themselves.



-- 
Steven.