Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <9507131940.AA20730@easynet.crl.dec.com>
Date: Thu, 13 Jul 95 15:47:20 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" <leonard@ricks.enet.dec.com>
To: info-hol@leopard.cs.byu.edu
Apparently-To: info-hol@leopard.cs.byu.edu
Subject: Using HOL badly

The discussion about making HOL easier to use is missing something important:
What's your intended market for HOL?  In particular, how much do you expect new
users to know about proof, and how much effort are you going to insist they
invest before being able to use HOL?  I think HOL works fine for most of the
kinds of people who are currently tempted to try it.  If you want to reach a
different market, determine what the market is.  Until you've done that, you
can't say what their needs are.

Having said that, I'll assume you want HOL to be easier to use for people who
currently design software or hardware, and who don't have a background in
formal methods.  I think HOL could be better suited for such people.  I'll try
to explain how in two ways; one short, the other somewhat longer.


FIRST TRY:

It's not now (and it never will be) possible to use HOL well without learning
about hundreds of HOL procedures.  It's not now (and it never will be) possible
to learn about hundreds of HOL procedures without a great deal of effort.  So
don't try to change HOL so it can be easy to learn to use well, because that's
impossible.  Instead, see if there's a way of using HOL badly!  (A way that's
easy to learn and still lets you prove useful theorems.)  If a novice must be
able to prove useful theorems, and will only learn 20 (or 40, or whatever)
commands, what commands should those be? 


SECOND TRY:

It seems to me that the HOL documentation is currently structured for people
who will someday learn how to use HOL well --- it introduces the underlying
objects and mechanisms, and builds on those until the user can create proofs
and proof tools.  (I'd say it does it pretty well, too.)  That may be the wrong
approach for people who may or may not learn how to use HOL well --- such
people must learn so much before being able to do anything useful that they may
well choose not to use HOL.  An alternative approach is to introduce a very
small number of mechanisms for creating proofs, and to get new users started,
and only later to explain what's really going on.  This assumes that there is
some small set of mechanisms that is sufficient for proving useful theorems,
and that even a novice can learn to recognize when each can or should be
applied. 

In my opinion, the ML interface to HOL should be irrelevant to novices.  A
point-and-click interface is sufficient.  (If the objects, operations, and
modifiers can be made orthogonal, then users can easily express what they're
trying to do.  In the ML interface, users discover that an operation is unsound
or meaningless by failing to find a function to perform it, or at best by
receiving an error message.  Better would be if meaningless or unsound 
operations responded by explaining why they were meaningless or unsound, and
suggesting alternatives.)  Of most importance is choosing the set of mechanisms
for novices to learn and use.  It will help greatly if it's possible for 
novices to recognize (without trying and failing) when a goal is not of the
right form to attack with the minimal tools.

Only once users can successfully (if tediously) prove theorems does it make
any sense for them to learn how to automate their methods.  For this, the ML
interface is necessary, but knowledge of the vast majority of HOL's ML
procedures is still unnecessary (though, of course, it's a great help).

The user should be able to choose when (if ever) to learn about the hundreds
of existing ML procedures.  After all, they exist only to increase the user's
(and HOL's) efficiency.


Tim