proving programs correct

["Perry E. Metzger" <perry@panix.com>]

A boss of mine at Bellcore, and a very smart guy (B. Gopinath) once
mentioned to me that (with the exception of scheme) he'd never seen a
set of formal semantics for a language that were smaller than the
largest program one would care to write in the language. He was, of
course, slightly exagerating for effect, but his point was very
simple: you can't even get the basis on which to write your proofs
right.

An interesting experience happened during the same project, as I
recall: we attempted to prove a small bit of code correct.
Unfortunately, the proof had a bug in it which meshed nicely with a
bug in the program and a bug in the implementation. Proofs are no less
large complicated formal constructs than programs are, and checking
them is no less onerous, unless they are written in formal logic in
which case they are not possible for human beings to produce.

Perry