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 ------------- -- http://mail.python.org/mailman/listinfo/python-list
