Re: return in loop for ?

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/

.