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

[Steve Holden]

John Nagle wrote:
> Juergen Erhard wrote:
>> On proving programs correct... from my CS study days I distinctly
>> remember thinking "sure, you can prove it correct, but you cannot do
>> actual useful stuff with it".  We might have come a long way since
>> then (late 80s :P), but I don't hold out much hope (especially since
>> the halting problem does exist, and forever will).
> 
>     The halting problem only applies to systems with infinite memory.
> 
>     Proof of correctness is hard, requires extensive tool support, and
> increases software development costs.  But it does work.
> 
>     Check out the "Spec#" effort at Microsoft for current work.
> Work continues in Europe on Extended Static Checking for Java,
> which was developed at DEC before DEC disappeared.
> 
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.

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.

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 -------------