Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 26 May 94 11:36:26 EDT
From: mel@ultrastar.EE.CORNELL.EDU (Miriam Leeser)
Message-Id: <9405261536.AA09235@ultrastar.EE.CORNELL.EDU>
To: hol2000@leopard.cs.byu.edu
Cc: nuprlnotes@cs.byu.edu
Subject: assumption numbering, user interfaces ...


In the Nuprl group we have been spending a fair amount of time on some
of the issues people have been discussing, particularly representing
proofs, lists of assumptions, and user interfaces.

Nuprl uses numbers to refer to assumptions (well, we call them
hypotheses but ...).  In my experience the problem with this is that
if definitions or proof steps change your tactic may break because it
refers to the wrong assumption.  In Nuprl, when a tactic breaks you
lose the remainder of the proof tree.  I believe that numbering
assumptions is an efficient way to refer to them internally, but users
should refer to them either by name or by content.  We have been
fairly successful in writing high level tactics in Nuprl that do NOT
explicitly use assumption numbers.  Nuprl 4 allows you to label
assumptions and refer to them, and this is a useful feature.

We have also spent a lot of effort over the last few years developing
a very sophisticated user interface.  The advantage of this is that
you have nice display forms that allow you to define formulas that
look the way the would in a Mathematics text, windows that allow you
to have multiple proofs open at once, tools for manipulating proof
trees, etc.  The disadvantage is that you need to learn a specialized
user interface just to use Nuprl.  I believe that the logic engine can
and should be separate from the user interface.  Ideally a user should
be able to choose among a variety of user interfaces.  For example, I
would like to see the Nuprl group develop an emacs-19 interface which
obviously will not have all the bells and whistles of the existing
interface, but which would give a user sufficient support to use the
hardware verification library we have been developing (and other
similar libraries too of course).  The HOL group ought to be able to
make use of the user interface developed for Nuprl, or at least much
of the experience.

As far as types are concerned I would like to see HOL have a richer
set of types.  We have found dependent types very useful for hardware
verification.

Some of these ideas are expressed in my paper (with Mark Aagaard and
Phil Windley) in the HUG93 paper called Toward a Super Duper Hardware
Tactic.  

Miriam Leeser
mel@ee.cornell.edu