Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!wuarchive!cs.utexas.edu!uunet!twwells!bill
From: bill@twwells.com (T. William Wells)
Newsgroups: comp.std.c
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <1989Nov10.185759.8031@twwells.com>
Date: 10 Nov 89 18:57:59 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> <1989Nov9.201125.8989@utzoo.uucp>
Organization: None, Ft. Lauderdale, FL
Lines: 15

In article <1989Nov9.201125.8989@utzoo.uucp> henry@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@twwells.com