Path: utzoo!utgpu!utstat!jarvis.csri.toronto.edu!mailrus!wuarchive!gem.mps.ohio-state.edu!samsung!aplcen!haven!adm!smoke!gwyn
From: gwyn@smoke.BRL.MIL (Doug Gwyn)
Newsgroups: comp.std.c
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <11571@smoke.BRL.MIL>
Date: 9 Nov 89 06:06:14 GMT
References: <11065@riks.csl.sony.co.jp> <2727@cbnewsl.ATT.COM> <11477@smoke.BRL.MIL> <11081@riks.csl.sony.co.jp> <11555@smoke.BRL.MIL> <1989Nov8.222632.699@algor2.algorists.com> <1989Nov8.225008.793@algor2.algorists.com>
Reply-To: gwyn@brl.arpa (Doug Gwyn)
Organization: Ballistic Research Lab (BRL), APG, MD.
Lines: 9

In article <1989Nov8.225008.793@algor2.algorists.com> jeffrey@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.