FOM: Program verification

[Andrzej Trybulec]

On Thu, 27 Jan 2000, charles silver wrote:

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

The goal of program verification is not to guarantee that the program is
correct, but to find bugs, and the to make a program a bit more reliable.

And it seems that most of programs have bugs. If not all.

My personal experience with computer controlling planes it not so bad (I
am still alive). Once in Narita computer claimed that doors are open and
the crew could do nothing about that. Well, after 20 minutes they
restarted the computer and eventually we took off. It was fun on the
ground, but something similar in the air...

Anyway planes crash because of bugs in programs. If the number of
accidents goes down two times, it will be a real gain.

The profit of software houses seems to be big enough to pay both for
verification and for other methods: testing. Let us try to do a rough
estimation (I think about Borland's Pascal, but I do not know if numbers
are exact).

The academic Pascal compilers (the source codes were published, e.g.
the 2 release of Pascal for CDC written by Urs Amman) have length about
10,000 lines. The proof of correctness is perhaps 100 times longer,
so let say the proof is 1 mln lines. 10 USD for a line seems to be a fair
price. Therefore the cost is 10 mln USD. It is nothing. If the product is
sold in 10 mln copies with the price 200 USD that for verified product you
have to pay 201 USD.

I have no idea how much money is spent for program verification, I think
anything below 10 billion USD per year would be not too much. Actually it
may be 10 mln USD. Or more? 

Instead of fighting against program verification (and taking the 
responsibility, the scholars do not like this very much) it would be
better to press the software producers to sell verified programs.

Of course I have some ulterior motives:
I heard an opinion, not once, that program verification is the most
important (the only important) challenge for mathematics in this century
and if mathematicians fail, the government should stop cut all money for
mathematics. And I would like to get my salary.

Andrzej Trybulec