NetNews Usenet Archive 1992 #20/NN_1992_20.iso/spool/comp/lang/cplus/13335

Internet Message Format | 1992-09-08 | 2.7 KB

Path: sparky!uunet!cis.ohio-state.edu!pacific.mps.ohio-state.edu!linac!att!att!allegra!alice!ark
From: [e-mail] (Andrew Koenig)
Newsgroups: comp.lang.c++
Subject: Re: GOTO, was: Tiny proposal for na
Message-ID: <[e-mail]>
Date: 5 Sep 92 17:04:34 GMT
Article-I.D.: alice.23634
References: <714668024@thor> <[e-mail]> <[e-mail]> <[e-mail]> <rmartin.714931485@thor> <[e-mail]> <rmartin.715102882@thor> <[e-mail]>
Reply-To: [e-mail] ()
Organization: AT&T Bell Laboratories, Murray Hill NJ
Lines: 41

In article <[e-mail]> [e-mail] (James Kanze) writes:

> Bob, don't you realize that Bill has just given the strongest argument yet
> in favor of what you've been saying.  The only "clear and convincing argument
> that the code is correct" must use logical proof of correctness concepts.
> These concepts, at least in the literature I've seen, *only* address the three
> basic forms of program flow: sequence, iteration and conditional.

But since every program can be mechanically rewritten in that form,
it doesn't matter.  Moreover, if we do grant your premise, we might
argue that it is even easier to prove programs correct if we eliminate
iteration, which after all can always be expressed by recursion.
[Indeed, there is now a whole family of languages that do just that]

Incidentally, this whole discussion harks back to a debate that appeared
a number of years ago in ACM Software Engineering Notes.  It began with
an article called `Social Processes and the Proofs of Theorems and Programs'
(or something like that) by DeMillo, Lipton, and Perlis.  Among the points
in that article:

    The mathematical community does not automatically accept
    formal proofs as establishing truth; the proof might be wrong.
    Rather, they insist that the result fit in with their existing
    framework of knowledge.  In effect, new theorems are established
    primarily by social means -- a formal proof is important but
    not sufficient by itself.

    Similarly, if a program spits out a 20,000-line proof of the
    `validity' of some other program, is that going to convince
    anyone that the program is actually correct?  They argue no:
    if nothing else, it is necessary to show that what was proved
    is actually the property that the author wanted the program to have.

This article was the subject of a rebuttal from Edsger Dijkstra that
was so strident and emotional as to detract from its credibility.
The article was called `On a Political Pamphlet from the Middle Ages,'
and its tone was consistent with the title.  That led to a re-rebuttal,
and so on.  Fascinating reading.
--
                --Andrew Koenig
                  [e-mail]