Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: Phil Windley <windley@cs.byu.edu>
Cc: shaw@cs.ucdavis.edu, info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: Easy theorem-provers -- not the Soft. Eng. answer
In-Reply-To: Your message of "Fri, 14 Jul 1995 06:22:31 MDT." <199507141222.AA138094551@bobcat.cs.byu.edu>
Date: Fri, 14 Jul 1995 17:25:17 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:151020:950714171113"@cl.cam.ac.uk>


> All I'm asking for is something like the PVS "grind" that removes the
> tedium.   We have some nice libraries that actually go a long way toward
> the gaol, but, IMHO, not far enough.  This is not a question that needs
> lots of market research.  ...

Quite.  There are many sensible and uncontroversial things that can be
done to raise the level interaction with HOL.  Really, it's all quite
feasible and straightforward, although inevitably we will need some new
research (e.g. for integration).

My question is the following.  Suppose we actually do go ahead and 
implement the obvious things (in, say, hol90).  The key issue is
will the user community be willing to put up with the numerous changes 
to the system that this will inevitably entail?  Suppose that there
were a compatability advice service on offer, to provide at least some
help when you upgrade to each new release?   

These are not mere theoretical questions.  I believe that, one way
or the other, HOL will begin fairly soon to evolve towards hol2000.
And input into this process from you, the user community, will be
crucial.  

As regards the learning curve issue, it has been be my approach when
giving HOL training courses to cover everything very thoroughly from
the bottom up.  In a sense, I still believe that this is good -- it
gives the user unparalled depth of understanding and the intellectual
tools to take best advantage of HOL's secure extensibility.  In a way
(as Tim points out) the structure of the documentation also reflects
this attitude towards teaching HOL.

I do, however, recognize that there is now a class of users (or potential
users) who just want to get started proving things as quickly as possible.  I
believe that we can, with some work on upgrading the existing infrastructure
(as alluded to above) quite easily cater for these users too.  Moreover,
when these users are ready to move on, we can deepen their understanding
of the system.  

As regards the interface, I believe this is very important.  But we
still need a lot of foundational investigation...

Tom