FOM: Re: Re: Re: Godel, f.o.m.

[charles silver]

C Silver:
>>  One
> > thing I'm wondering about is how *often* a program is verified and
> > wrong.  That is, does anyone know how often mistaken verification
> > *actually* takes place?  My guess is, not often, though I concede
> > that it *can* happen.


S Stevenson:
>@article{social,
>  author = "R. A. DeMillo and R. J. Lipton and A. J. Perlis",
>  title = "Social Processes and Proofs of Theorems and Programs",
>  journal = "Communications of the ACM",
>  month = "May",
>  year = "1979",
>  volume = "22",
>  number = "5"
>}
>More or less parroting the CS testing line from deMilo: Of the
>thousands of proofs published every year, how many are without
>error. I've heard numbers like 10% from reliable math sources.


    Sorry, I didn't phrase my question properly.   How frequently does the
following occur:  there's a faulty proof P purporting to verify program M,
*and* M is incorrect.  For example, to take the kind of practical situation
you worried about earlier, how likely would it be to obtain a purported
proof P showing that the guidance system of a nuclear warhead operates
correctly, but the proof is incorrect and in fact the guidance system
doesn't work correctly?  I know that even if you have a *correct* proof,
there are reasons (pertaining to the operations of distinct compilers, etc.)
why the program still may not run properly.  But, I'm not asking that.
That's a separate question of interest.

    Incidentally, in an earlier message you suggested that Fetzer's argument
was appealing to persons like yourself with actual computer experience, as
opposed to people with little c.s. experience who were just trying to apply
formal mathematics to computer science.   I disagreed with that suggestion
earlier.  But, I want to call your attention to the fact that when he wrote
the paper Fetzer himself knew next to nothing about computers, and was
simply applying a formal, skeptical critique to computer programming.

Charlie