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

[John Nagle]

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.

				John Nagle