[SystemSafety] Fetzer

[David Crocker]

Several times I have been told "the Halting Problem proves that you
can't prove software is correct".

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 18/06/2019 19:33, Peter Bernard Ladkin 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
>
>
>
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190619/83fb5f01/attachment.html>