🚀 go-pugleaf

One interesting thing that Hendrik Boom mentioned to me from using his
(total correctness) verifier was that he typically found more bugs in
his SPECIFICATIONS than he did in his PROGRAMMES (for example, a sort
routine failed to typecheck because the specification failed to handle
duplicates correctly).

Now, you might think that this is a strike against verification (at
very least it suggests that writing short, abstract, mathematical
specs may NOT be easier than coding up a decent algorithm, and that
checking such a spec by eye may not be so straightforward), but in
fact it's precisely the spec (albeit in a less formal form) that is
going to be the interface contract between the routine and the outside
world.

The effect of the verifier, then, is to make you look VERY hard at the
properties of your interfaces.

And my experience has been that interfaces are the things that HAVE to
be right - the code you can always discard.
----------------------------------------------------------------------
stephen p spackman         Center for Information and Language Studies
systems analyst                                  University of Chicago
----------------------------------------------------------------------