Steven D'Aprano wrote: > On Fri, 25 Nov 2005 08:36:48 +0000, Steve Holden wrote: [...] > >>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. > No, I didn't mean to say that. Although of course there *are* issues surrounding the semantic edge cases to do with implementation on real hardware that do require formal theories to be limited and hedged with restrictions due to the restrictions if the underlying hardware, for example. Numerical analysts, though, have been well used to reasoning about differences between the theoretical behaviour of algorithms and the behaviour of their implementations for decades, so this is nothing new.
> 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. > Well naturally I can't stop you thinking that, so I won't try. > 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. > Your bald assertion fails to change my mind about that, but it is quite a fine theoretical issue. For what it's worth, I *have* discussed this issue with academic formal proof specialists, some of whom have admitted that it's a (theoretical) problem. But in the world of the practical I wouldn't disagree with your characterisation of the state of the art. 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
