PEP 3107 and stronger typing (note: probably a newbie question)

[Steve Holden]

Paul Rubin wrote:
> Steve Holden <steve at holdenweb.com> writes:
>> The issue I have with correctness proofs (at least as they were
>> presented in the 1980s - for all I know the claims may have become
>> more realistic now) is that the proof of correctness can only relate
>> to some highly-formal specification so complex that it's only
>> comprehensible to computer scientists.
> 
> Just like software as it is now, is only comprehensible to
> programmers.  A long while back there was a language called COBOL
> designed to be comprehensible to non-programmers, and it actually did
> catch on, but it was cumbersome and limited even in its time and in
> its application era, not so readable to non-programmers after all, and
> is not used much in new projects nowadays.
> 
The trouble there, though, is that although COBOL was comprehensible (to 
a degree) relatively few people have the rigor of thought necessary to 
construct, or even understand, an algorithm of any kind.

>> In other words, we can never "prove" that a program does what the
>> customer wants, because the semantics are communicated in different
>> ways, involving a translation which, since it is necessarily performed
>> by humans using natural language, will always be incomplete at best
>> and inaccurate at worst.
> 
> The types of things one tries to prove are similar to what is less
> formally expressed as localized test cases in traditional software.
> E.g. for a sorting routine you'd want to prove that output[n+1] >=
> output[n] for all n and for all inputs.  As the Intel FDIV bug
> incident reminds us, even billions of test inputs are not enough to
> show that the routine does the right thing for EVERY input.

Well I can buy that as a reasonable answer to my point. The early claims 
of the formal proof crowd were somewhat overblown and unrealistic, but 
that certainly doesn't negate the value of proofs such as the one you 
describe.

regards
  Steve
-- 
Steve Holden        +1 571 484 6266   +1 800 494 3119
Holden Web LLC/Ltd           http://www.holdenweb.com
Skype: holdenweb      http://del.icio.us/steve.holden
--------------- Asciimercial ------------------
Get on the web: Blog, lens and tag the Internet
Many services currently offer free registration
----------- Thank You for Reading -------------