Denotational Semantics and Language Standards
T. William Wells
bill at twwells.com
Sat Nov 11 05:57:59 AEST 1989
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
More information about the Comp.std.c
mailing list