Efficient python programming...

[Kragen Sitaker]

Peter Hansen <peter at engcorp.com> writes:
> Roman Suzi wrote:
> > To prove that code is correct is very difficult (practically impossible).
> > Unittests are there to prove that you have errors, not the other way
> > around.
> 
> I disagree, if the tests are written first (and run, proving that
> they will fail when the code is wrong or missing).

I think you are disagreeing because you are ignorant of formal methods.

> The tests are executable requirement specifications.  Running
> them "proves" (yes, not 100%... nothing could) that the code
> meets the specs.  The specs could be wrong of course, but that
> doesn't mean the code is broken...

Typically specs specify the behavior of the code in an infinite set of
situations.  Tests test the behavior of the code in a finite set of
situations, one situation per test.

You said "nothing could", but you are mistaken.  Computer programs are
sufficiently amenable to mathematical analysis that it is possible to
prove rigorously that a particular routine meets a particular spec,
100% of the time, if the spec is phrased in sufficiently rigorous
terms.

This has the following drawbacks:
- specs can be wrong (but if they're shorter than the code, they'll
  probably have fewer bugs)
- proofs can be wrong (but at least they make you think about the
  assumptions you made when writing the code)
- writing the proofs takes a long time, so long that it's practical
  only for small programs
- your proof is dependent upon your specification of the program's
  environment as well as upon your requirements specification; if your
  program depends on a lot of other complicated software, your proof
  may not be worth much

This is important not because rigorously proving a program correct is
a worthwhile activity --- maybe it is, but I'm not convinced --- but
because proving a program correct is a more rigorous version of what
good programmers do all the time in writing good code.  You should
learn a little bit about it, at least in its lighter-weight forms like
cleanroom programming.