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. -- http://mail.python.org/mailman/listinfo/python-list
