[SystemSafety] Fetzer

[Peter Bernard Ladkin]

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





-------------- 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/20190618/09d96fb9/attachment.sig>