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