return in loop for ?

[Steve Holden]

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/