🚀 go-pugleaf

"Proving your programs are correct" seems to mean different things
to different people:

One group thinks it means that your program does exactly what your
spec says it should.

Another group thinks it means that you can put complex assertions
in your code and have the checker makes sure that these assertions
are always true.

The first sort of proof is obviously useless, the spec becomes the
program, and bugs in the spec become bugs in the program.  Also,
specifing most programs is impossible; and if you could, then you
could write a compiler for the specification language.

The second sort of group is more interesting.  It has these advantages:
    It is possible.
    It is not all or nothing (simple assertions can added now, and 
        complex ones added later on).
And these disadvantages:
    Doing it well requires specific skills, which need to be taught.
    It will never prove correctness; it only proves that some assertions
        are true. 
    There are still problems getting test input data.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822