Denotational Semantics and Language Standards

[T. William Wells]

In article <1989Nov9.201125.8989 at utzoo.uucp> henry at utzoo.uucp (Henry Spencer) writes:
: 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.

Which leads us to: we finally would have a real use for all those
automatic theorem provers! 1/2 :-)

---
Bill                    { uunet | novavax | ankh | sunvice } !twwells!bill
bill at twwells.com