Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
From: Kathi Fisler <kfisler@cs.indiana.edu>
Subject: Re: Using HOL badly
To: info-hol@leopard.cs.byu.edu
Date: Thu, 13 Jul 1995 18:32:12 -0500 (EST)
In-Reply-To: <9507131940.AA20730@easynet.crl.dec.com> from "Tim Leonard, DTN 225-5809, HLO2-3/C11" at Jul 13, 95 03:47:20 pm
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 1199
Message-ID: <"swan.cl.cam.:006010:950713235531"@cl.cam.ac.uk>

> Only once users can successfully (if tediously) prove theorems does
> it make any sense for them to learn how to automate their methods.

In the case of those of us trained in formal methods, I disagree.  I
feel that the lack of decision procedures forces us to focus heavily
on the least interesting (and least educational, in some sense) part
of proof during the early stages of learning HOL.  I spent three weeks
trying to learn enough HOL to carry out a simple hardware proof.  This
was a proof I had done previously as a novice PVS user (in a matter of
days).  At the end of the three weeks, I had managed to only discharge
one or two simple parts of the proof.  I gave up, largely out of
frustration with the lack of decision procedures, and have been a PVS
user ever since.

I am not trying to spark a HOL versus PVS debate here.  I just feel
that, unless you are prepared to devote considerable time to learning
HOL, even a trained formal methods person can find the learning curve
to be too steep.  I think this especially would hold true for users
who want to use theorem provers on occasion, rather than on a more
steady basis, even if those users are already in formal methods.

Kathi