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