[SystemSafety] Fetzer

[Littlewood, Bev]

Hi Peter

Just read Fetzer’s Wikipedia entry. Appalling stuff indeed.

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 recall thinking at the time that much of it made sense. My main recollection, though, is that it was very funny.

Cheers

Bev

On 18 Jun 2019, at 19:33, Peter Bernard Ladkin <ladkin at causalis.com<mailto:ladkin at causalis.com>> wrote:


Some of us are old enough to remember the brouhaha caused by the CACM publishing an article in 1988
by the philosopher James H. Fetzer claimed two things: (a) program verification is impossible, and
(b) therefore the USG should stop funding it.

I thought, and still do, that (a) has a simple two-line refutation (OK, five lines. The proof is two
lines, but the set-up takes three). Namely, that when you verify a program (we mean here a real
honest-to-goodness program, something that executes on HW) you compare two things, the program with
some sort of specification S. And if S happens to be logically equivalent to TRUE, there is a
one-inference proof in propositional logic that your program is correct. Ergo verification is prima
facie possible.

It is also not the sole criterion for dependability: you need also to check that your specification
is correct.

It is now generally agreed that program verification is indeed a comparison of a program with some
kind of specification. (I think it was then; it is clearly expressed in Barry Boehm's SEE.)

Fetzer's argument completely omitted considering specifications, which is why it fails.

Somehow, my two-line refutation didn't win acceptance amongst SW engineers (Cliff may remember) and
it never got published. But I was old and foolish then, and I'm younger than that now.

And where is Fetzer? Writing books that the Sandy Hook massacre never happened, and losing in court.
https://www.theguardian.com/us-news/2019/jun/18/sandy-hook-massacre-victim-father-wins-defamation-lawsuit

PBL

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





_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE<mailto:systemsafety at TechFak.Uni-Bielefeld.DE>
Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety

_______________________________________________

Bev Littlewood
Emeritus Professor of Software Engineering
Centre for Software Reliability
City, University of London
EC1V 0HB

_______________________________________________

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190619/db55d532/attachment-0001.html>