Denotational Semantics and Language Standards

[Doug Gwyn]

In article <1989Nov8.225008.793 at algor2.algorists.com> jeffrey at algor2.ALGORISTS.COM (Jeffrey Kegler) writes:
>...  A brave new world, where any question about dpANS could be stated
>as a theorem and proved or disproved ... would seem a vast improvement.

An additional drawback that you failed to mention in your article is
that C is deliberately "fuzzy" in many areas, to permit efficient
implementation on a variety of architectures.  This makes it rather
unsuitable to theorem proving, since useful theorems would have to be
about C's behavior on entire classes of architectures.