Denotational Semantics and Language Standards

[Doug Gwyn]

In article <1989Nov9.201125.8989 at utzoo.uucp> henry at 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!