From: hallam@w3.org
To: cypherpunks@toad.com
Message Hash: eccb215a2f3902b554467cb5d3cc422d8743fca1fb37b0384f63a264a6e22e4a
Message ID: <9508081749.AA20619@zorch.w3.org>
Reply To: <199508081248.IAA11447@panix2.panix.com>
UTC Datetime: 1995-08-08 17:55:49 UTC
Raw Date: Tue, 8 Aug 95 10:55:49 PDT
From: hallam@w3.org
Date: Tue, 8 Aug 95 10:55:49 PDT
To: cypherpunks@toad.com
Subject: Re: proving programs correct
In-Reply-To: <199508081248.IAA11447@panix2.panix.com>
Message-ID: <9508081749.AA20619@zorch.w3.org>
MIME-Version: 1.0
Content-Type: text/plain
>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
Return to August 1995
Return to ““Perry E. Metzger” <perry@panix.com>”