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

[John Nagle]

Chris Mellon wrote:
> You can't prove a program to be correct, in the sense that it's proven
> to do what it's supposed to do and only what it's supposed to do.

     Actually, you can prove quite a bit about programs with the right tools.
For example, proving that a program cannot subscript out of range is
quite feasible.  (Although not for C, where it's most needed; that language
is just too ill-defined.)  You can prove that certain assertions about
an object always hold when control is outside the object.  You can
prove that certain entry conditions for a function are satisfied by
all its callers.

     Take a look at what the "Spec#" group at Microsoft is doing.
There's also some interesting USAF work on avionics at

http://www.stsc.hill.af.mil/crossTalk/2006/09/0609SwardGerkenCasey.html

But it's not a very active field right now.  The basic problem is that
C and C++ aren't well suited to proof of correctness, yet none of the
other hard-compiled languages have any significant market share left.

      This is irrelevant to Python issues, though.

					John Nagle