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

[John Nagle]

Paul Rubin wrote:
> 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.

     Ah. At last, an intelligent comment about program proving.

     One of the biggest problems with proof of correctness is that,
as a first step, you need a language where you don't have to "lie to
the language".  That is, the language must have sufficient power to
express even the ugly stuff.

     Python isn't bad in that regard.  A good example is the "struct"
module, where you can explicitly convert a string of bytes into a
Python tuple.  That's an inherently risky operation, but Python has
a safe and unambiguous way to express it that doesn't depend on the
machine representation of Python types.  In C and C++, this is often
done using casts, and what's going on is neither explicit nor checked.
Note that it's quite possible to implement something like the "struct"
module for C, and it could even be compiled into hard code.  (GCC,
for example, knows about "printf" strings at compile time, so that's
not an unacceptable idea.)

     The big problem with C and C++ in this area is the "array=pointer"
convention.  Again, that's lying to the compiler.  Programmers have to
write "char* p" which is a pointer to a char, when they mean an array
of characters.  That's inherently wrong.  It was a good idea in the 1970s
when it was developed, but we know better now.

     If you were doing proofs of correctness for Python, the biggest headache
would be checking for all the places where some object like a module or function
might be dynamically modified and making sure nobody was patching the code.

     Enough on this issue, though.

					John Nagle