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

[Paul Rubin]

Kay Schluehr <kay.schluehr at gmx.net> writes:
> Sure. But knowing that memory is limited doesn't buy you much because
> you achieve an existential proof at best: you can show that the
> program must run out of memory but you have to run the program to know
> where this happens for arbitrary input values. Moreover you get always
> different values for different memory limits. So in the general case
> you can't improve over just letting the program run and notice what
> happens.

Program verification is nothing like the halting problem.  It's not
done by dropping the program into some tool and getting back a proof
of correctness or incorrectness.  The proof is developed, by the
programmer, at the same time the program is developed.  Verifiability
means that the programmer-supplied proof is precise enough to be
checked by the computer.

Think of when you first learned to program.  Most non-programmers have
an idea of what it means to follow a set of steps precisely.  For
example they could tell you an algorithm for sorting a shelf full of
books alphabetically by author.  Programming means expressing such
steps in much finer detail than humans usually require, to the point
where a machine can execute it; it takes a lot of patience and
knowledge of special techniques, more than non-programmers know how to
do, but we programmers are used to it and even enjoy it.

Now think of something like a code review.  There is a line of code in
your program (maybe even an assert statement), that depends on some
variable "x" being greater than 3.  You must have had a reason for
thinking x>3 there, so if the reviewer asks why you thought that, you
can explain your argument until the reviewer is convinced.

Do you see where this is going?  Code verification means expressing
such an argument in much finer detail than humans usually require, to
the point where a machine can be convinced by it; it takes a lot of
patience and knowledge of special techniques, more than most of us
regular "practical" programmers currently know how to do, but the
methods are getting more accessible and are regularly used in
high-assurance software.  In any case there is nothing magic about
it--just like programming, it's a means of expressing precisely to a
machine what you already know informally how to express to a human.