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

[Vaughan Pratt]

Charles Silver:
CS>I guess a more direct question is to ask whether people think that the
CS>formal approach to program verification is of value at all, given the many
CS>kinds of errors that can creep in.  Are the benefits of program verification
CS>outweighed by its weaknesses and costs?  Or, given that you have a certain
CS>amount of money to spend for assuring program correctness, would the money
CS>be better spent looking for other test mechanisms than for formal
CS>verifications?

In the program verification community the old role of program verification
as a sort of "seal of good programming" has been superseded in recent
years by its new role as bug finder.  The old job description was "decide
whether the given program is correct."  The new description is the visibly
more constructive one of "enumerate the bugs in the given program."

Under the old scenario, a programming team working on any sufficiently
serious program is confronted with the extremely difficult if not humanly
impossible task of making the program perfect before it will pass muster.

The new scenario instead gives insight into what can go wrong with a
system and what might be done about it when this presents a sufficiently
serious problem.  One might for example wish to fix the more potentially
more harmful bugs, and to merely warn users about the presence of more
innocuous bugs.

This is clearly a move away from perfection that allows for example
erroneous judgment calls to be made about severity of bugs.  Nevertheless
this is a distinct improvement over the situation where one is not even
aware of bugs in the system.

The nice thing about this approach from the logical standpoint is
that logic continues to play an important role.  Furthermore because
this approach is more useful than the old perfection-or-bust approach
criticized with some justification by Lipton, de Millo, and Perlis, this
translates to an increase in the practical utility of the underlying
logical methods common to both approaches.  It's a win-win situation
for both software engineers and logicians.

Vaughan Pratt