proving programs correct

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

>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.


I suggest he look at occam, the semantics are very compact, about ten pages.

The purpose of writing the denotational semantics is to obtain a grounding for 
the axiomatic semantics which may then be used for proofs.

All this means is that languages such as ADA are useless for formal methods work 
because the language is too big to develop a usefull semantics for it. C is 
better but still far too large and the semantic ambiguities of the language 
cause problems.

I don't consider the conventional application of formal methods to be a 
practical approach. This does not mean that no such approaches exist, merely 
that people use the wrong ones.


		Phill H-B