Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Tue, 12 Jan 93 16:45:56 PST
From: Paul.Loewenstein@COM.Sun.Eng (Paul Loewenstein)
Message-Id: <9301130045.AA02034@lara.Eng.Sun.COM>
To: slind@de.tu-muenchen.informatik, info-hol@edu.uidaho.cs.ted
In-Reply-To: Konrad Slind's message of Wed, 13 Jan 1993 00:05:52 +0100 <93Jan13.000602met.8121@sunbroy14.informatik.tu-muenchen.de>
Subject: BETA_CONV
Content-Length: 1797


Konrad Slind says, taken out of context:

>  In my opinion, and I'm totally off topic here (and
> perhaps flagrantly wrong!), the bottleneck in the HOL system these days
> is not the system; it's the user and the low level at which they
> operate. Take the library of sets for example: it takes hol90 approx. 45
> seconds to prove all the theorems in the library. How long did it take
> to write the proofs?


For typical "mathematical" proofs this seems to be true.  However for
many interesting hardware proofs HOL is still a major bottleneck.

I have been running model checker proofs with case analyses
approaching 25x10^6.  HOL cannot cope with tedium at this level.
Although the power of HOL can usually be used to reduce the number of
cases, for typical concurrent systems there appears to be no workable
compromise using a HOL-style theorem prover.

Brute force takes too long to execute, and cunning takes too long to code.

For the moment I am using model checking until I can think of a better
way forward.

A pragmatic approach would be to hard code selected proof procedures,
bipassing the inference rule mechanism, but that opens up a maintenance
nightmare.

How about reflection as a means of introducing robust and efficient
proof procedures?  Having written a reasonably efficient BDD verifier
in SML, it did not appear to be too difficult (in principle) to prove
sound.  It used some imperative code, but mostly in a way that
affected only efficency, not soundness.  The most difficult part to
prove correct is the function memoisation.  The BDD hash table
maintenance had no effect on soundness, it just made the difference
between constant and exponential time for many operations.


	Paul Loewenstein -- paul.loewenstein@Eng.sun.com

        Staff Engineer, Sun Microsystems