PEP 3107 and stronger typing (note: probably a newbie question)
nagle at animats.com
Fri Jul 20 06:45:39 CEST 2007
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.
More information about the Python-list