Denotational Semantics and Language Standards

[Henry Spencer]

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 (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 at zoo.toronto.edu