[SystemSafety] Fetzer

[Peter Bernard Ladkin]

On 2019-06-19 16:30 , Littlewood, Bev wrote:
> 
> But your posting here reminded me of reading the DeMillo, Lipton and Perlis CACM paper, ten years
> before Fetzer’s (40 years ago!). What are your thoughts on this now? 

I just re-read it.

Their observations that, and how, mathematical proofs are different creatures from what is needed in
the formal verification of a computer program are pretty accurate, well-sourced, and I suspect this
needed urgently to be said. Half a decade later, Leslie Lamport was pointing out that in fact
mathematicians don't provide proofs of the sort needed for program verification. But his conclusion
was different: not that you can't do program verification very well, but that mathematicians only
think they prove things; they don't always check very well and in fact it is only the ATP people who
do real proofs. His example was an elementary assertion in the introduction to John Kelley's
pervasive book General Topology. When I saw him give this talk at Berkeley, he got into an
entertaining discussion with VelVel Kahan, who didn't agree with this proposition at all. Other
Turing Award winners in the room were Dick Karp and (to be) Manuel Blum. Lots of fun.

I'm with Leslie - and Larry Paulson, Toby Nipkow, Georges Gonthier et al. - on what it takes to
really prove something. And with everyone (including DeMillo et al.) on the impenetrability of
formal proofs of programs. But in contrast with DeMillo et al., I don't think this impenetrability
is much to be worried about (as David Crocker has just pointed out on the list).

So I think they got wrong what formal verification is about. But it is not surprising that, after
forty more years of evolution, we know rather more about it.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190619/a442c8c9/attachment-0001.sig>