Newsgroups: comp.std.c
Path: utzoo!henry
From: henry@utzoo.uucp (Henry Spencer)
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <1989Nov9.201125.8989@utzoo.uucp>
Organization: U of Toronto Zoology
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>
Date: Thu, 9 Nov 89 20:11:25 GMT

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 (or, much less likely, found undecidable), would seem a vast
>improvement.

Maybe.  Remember that "proved" and "disproved" should really read "claimed
to be [dis]proved" -- only God can consistently write error-free proofs.
Certainly human mathematicians and program-verification people don't, as
witness quite a few embarrassing errors in formally-refereed published
papers purporting to be demonstrations of how to verify programs!

A formal definition of C would inevitably be large and messy, especially
given the many places where C refuses to promise how the machine behaves.
I suspect that proving theorems from it would not be a simple exercise.
-- 
A bit of tolerance is worth a  |     Henry Spencer at U of Toronto Zoology
megabyte of flaming.           | uunet!attcan!utzoo!henry henry@zoo.toronto.edu