Path: utzoo!attcan!uunet!cs.utexas.edu!uwm.edu!rpi!brutus.cs.uiuc.edu!ux1.cso.uiuc.edu!ux1.cso.uiuc.edu!m.cs.uiuc.edu!p.cs.uiuc.edu!johnson
From: johnson@p.cs.uiuc.edu
Newsgroups: comp.object
Subject: Re: Reasons why you don't prove your pr
Message-ID: <135300023@p.cs.uiuc.edu>
Date: 14 Jan 90 01:38:22 GMT
References: <7578@hubcap.clemson.edu>
Lines: 42
Nf-ID: #R:hubcap.clemson.edu:7578:p.cs.uiuc.edu:135300023:000:2012
Nf-From: p.cs.uiuc.edu!johnson    Jan 12 23:09:00 1990


Arguments that program verification is impossible because the
halting problem is undecideable are silly.  Don't you think that
the people who work(ed) on program verification knew that?  
Just because it isn't possible to verify every program doesn't
mean that it isn't possible to verify all the programs I want
to verify.  Undecideability is with a class of problems, not
individual problems.

There are lots of good arguments against 1970's style verification.
The best (to me) is that proving the equivalence of two programs
is not really interesting, and that is essentially what proving that
a program meets its complete specification is about.

A more general argument is that most system bugs are due to bad
specifications, not bad implementations of good specifications.
Thus, worrying about verification is a waste of time.  This is
a less compelling argument because, after all, there are quite a
few implementation errors, even if most errors are design errors.

One of the popular approaches to developing verified code today
is to start with the specifications and to transform it into a
program.  The idea is that the specification is a sort of program,
only extremely inefficient, and the transformations make it efficient.

Another is the idea of developing the program and the proof hand
in hand, but not necessarily making them equivalent, as the first
approach tends to do.

Then there was the idea expressed earlier of just letting the
system verify that certain assertions were true.  I like this
approach because you could combine it with Eiffel-style assertions
and a good optimizing compiler to eliminate a lot of checks and
make programs faster.

I think everybody (except Dijkstra) would agree that it isn't
currently practical to verify the correctness of large programs.
Nevertheless, I think that verification technology is important now
because it helps us think about programming better, and it might be
an important part of the way we build systems in the future.

Ralph Johnson