Re: proving programs correct

[hallam@w3.org]

>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