Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
To: info-hol@cs.uidaho.edu
Subject: HOL improvement survey results
Date: Wed, 13 Oct 93 17:17:13 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:139840:931013161759"@cl.cam.ac.uk>


Here at last is a summary of replies to the HOL improvements survey. 5 people
replied, and I have inserted their comments, often verbatim, under loose
categories. Some suggestions have been omitted if they are clearly subsumed by
others.

John.

-----------------------------
General/philosophical remarks
-----------------------------

Attention should be given to making HOL proofs more readable and closer to the
ordinary "textbook style" presentation.

--------------------
Logic/theory changes
--------------------

Numerals should be implemented by prettyprinting of a list representation.

Proper abstract theories would be useful and TFM's quantified types seem like
they would be interesting. They both seem to require changes in the logic to be
handled properly, though. Could there be a system where both are consistently
accommodated?

Reflection principles are a long-term goal. Proper ones are bound to lie years
in the future, while the "logic of SML programs" gets sorted out. Simpler
efforts based on identifying the "executable" subset of functions of HOL and
reasoning about them as a basis for reflection is possible.

Isabelle-style logic variables could be tried, although there might be a
work-around that would enable us to keep the same term structure.

Proving correctness of the base implementation. This will soon be possible, in
that soon there will be a basis small enough to be reasoned about.

Overloading. My opinion is that one can be happy with quite limited forms of
this, but there are other proposals to consider, such as type classes.

We ought to develop a notion of goal at the theory level, in order to handle
large-scale theory development.

---------------------
Specific enhancements
---------------------

The list library should be cleaned up and fleshed out.

The extract-field and insert-field operations on wordn should return wordn, not
words the size of the extracted field.

The way associativity theorems are written should be made uniform (e.g.
ADD_ASSOC and ADD_ASSOC are the opposite way round).

AC_CONV should instantiate polymorphic theorems.

The "pair" and "res_quan" libraries should be moved into the core system. (And
combined so one can deal with restricted pairs).

Pairing and restricted quantification ought to be supported uniformly
throughout the system. Actually, all type constructors should be usable as
pattern-formers.

The "res_quan" stuff should be improved.

There should be easy controlled ways of restricting the effect of resolution,
both on canonicalization of the theorems, which new theorems get added to the
assumption list, and which assumptions are used.

We need an implementation of higher-order matching, so that MATCH_MP_TAC can be
more useful in applying rules in object-logics.

We need more principles of definition in the system. Definition by well-founded
recursion and pattern matching is important. Mutually recursive definitions are
important, as is the "broader" class of trees introduced by Elsa Gunter at the
last workshop.

We need more flexibility in parsing and prettyprinting, especially when
different object languages need to be supported. Maybe an Earley-style parser
as in Isabelle would be appropriate. Right now, all that can be done is to
change the parser by hand. This is a bit clumsy, requires programming, and
doesn't fit in well with the library system.

We need a simple, portable graphical user interface.

xholhelp is really nice, but it needs sprucing up. It would be nice if xholhelp
could automatically keep track of the new help that becomes available when a
library gets loaded in, but that might require bringing xholhelp into SML.

We need separate compilation of libraries for hol90.

Theory files need to do a better job of sharing - they are too large and take
too long to load.

The concrete syntax of strings needs to be settled.

The library system seems quite complex. Can it be simplified?

The installation procedure needs to be simpler. We will want to be able to send
theories around to our friends - how can this be done securely?

The prettyprinter needs to be able to emit Latex, or Postscript. (And the
parser?)

Better error messages on type inference failure.

Programmability of the lexer. In hol90, there is not as much flexibility for
this as in HOL88.

We need a better interface to proof than the goalstack.