PEP 3107 and stronger typing (note: probably a newbie question)
Steve Holden
steve at holdenweb.com
Fri Jul 20 10:11:37 EDT 2007
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 -------------
More information about the Python-list
mailing list