Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Sun, 16 Jul 1995 15:36:30 -0500 (EST)
From: renneber@aals01.alcatel.oz.au (Carl Renneberg)
Subject: Re: making theorem provers easier to use
To: info-hol@leopard.cs.byu.edu
Cc: renneber@cim.alcatel.oz.au
Content-Transfer-Encoding: 7BIT
Message-ID: <"swan.cl.cam.:030360:950716055214"@cl.cam.ac.uk>


 Konrad Slind <slind@informatik.tu-muenchen.de> wrote:
> ... 
> Anyway, to address the wider discussion, by ENOD I think that most of
> the impressive achievements in formal verification are due to the
> persistence AND mathematical talent of the humans doing the
> formalizations and proofs. The following fact is worth pondering: many
> of the most significant verifications have been performed by people
> working at an *extremely* low level of automation. It is not clear to me
> that making proof systems with better user interfaces or more decision
> procedures will change that. Sure the naive user can be supported for a
> long time, but inevitably the user will be in a situation where the
> support doesn't do the right thing or just plain isn't there. At that
> point, the naive user is going to have a bad day.
> 

Konrad's comments make me think of SPICE, the famous analog circuit simulator.

I use SPICE occasionally. I'm not an expert in numerical methods or in
semiconductor device physics. And most of the time, I don't have to be. I
certainly don't need this expertise just to get started on simple circuit
problems.

Very occasionally, SPICE will "trip up" on certain circuits, or give results
which are at odds with lab measurements.  Then I *do* have to learn more about
the numerical methods that the simulator is using, and about the more advanced
device models; their subtleties; and the underlying physics.

But that's ok. Most of the time, the simulator does all of the tedious work
for me, and helps make me productive.

Now, I'd like to use HOL in the same way. I'd like to use it in my day-to-day
work (h/w and s/w for embedded systems), so that:

    - most of the time, I don't have to have a *deep* knowledge of HOL's
      internals;

    - HOL, or an application that runs on top of it, knows something about my
      problem domain (say, digital hardware), and shields me from the fiddly
      low-level details of the verification.

Occasionally, as Konrad points out, that won't work. And then I will have to
use HOL at a low level.

That's fine, if, most of the time, HOL does the tedious work, and helps make me
more productive.


> Don't get me wrong: I believe that automatic support is good, however, I
> don't think we should saddle ourselves with the pernicious belief that
> better automatic tools will lead us to the promised land where
> verification will be an easier task.

I don't understand why making verification easier is an unrealistic goal.
Surely HOL itself is a (magnificent) step towards it.


> We may be able to easily verify a larger number of trivial circuits or
> programs, but remember that we are trying to meet expectations that keep
> rising. We may make bigger steps in proofs, but the decisions to be made
> will still require well-informed and talented users.
> 

Sure. Not everyone can engineer proofs, or design hardware, or write software:
it takes talent, knowledge, experience, judgement, and good tools.

But I believe that the effort required of the tool user should be commensurate
with the difficulty of the problem. The tool itself shouldn't get in the way.
Novices should be able to solve simple problems with relatively little effort.


> The bad news is that verification will always be hard; the good news is
> that it may be hard in more interesting ways.
> 
> Konrad.
> 

Sounds like the promised land to me :-).

Carl.