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