Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!iuvax!purdue!haven!adm!smoke!gwyn
From: gwyn@smoke.BRL.MIL (Doug Gwyn)
Newsgroups: comp.std.c
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <11581@smoke.BRL.MIL>
Date: 10 Nov 89 19:15:05 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>
Reply-To: gwyn@brl.arpa (Doug Gwyn)
Organization: Ballistic Research Lab (BRL), APG, MD.
Lines: 12

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

My favorite was an example in Dijkstra's classic "A Discipline of
Programming" where he claimed that he hadn't submitted his program
to operational testing since it had been created using a discipline
that guaranteed it would be correct.  Naturally, there were a couple
of bugs in it!