Date: Mon, 12 Feb 1996 11:25:19 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Subject: Re: hol90 should have more control about proofs
In-reply-to: "Your message of Mon, 12 Feb 1996 01:00:06 +0100."
 <96Feb12.010012met.8161@sunbroy14.informatik.tu-muenchen.de>
Sender: info-hol-request@leopard.cs.byu.edu
To: Konrad Slind <slind@informatik.tu-muenchen.de>
Cc: info-hol@leopard.cs.byu.edu, reetz@ira.uka.de
Errors-to: info-hol-request@leopard.cs.byu.edu
Message-id: <E0tlwNk-000337-00@bescot.cl.cam.ac.uk>
MIME-version: 1.0
Content-type: text/plain; charset=us-ascii
Content-transfer-encoding: 7BIT
Precedence: list


Hi Konrad,

> > So, in the long run I believe it would be better to clearly
> > distinguish between user interaction languages and the implementation
> > language.  In the short term I think this applies expecially to theory
> > description files - HOL should be usable as a tool for making and
> > investigating specification, which it clearly is not at present.  The
> > ability to describe theories via a theory file format would help
> > things alot.
> 
> I sort of agree and I sort of don't. For one thing, math papers (are we
> trying to emulate them?) freely intermix the introduction of notation
> and definitions with proofs, whereas what I think is being discussed
> here would require the introduction of all definitions and syntax before
> beginning any proofs. This would pose a particular difficulty for HOL,
> since the principle of constant specification requires a theorem saying
> that the specification has witnesses, and often (always!) that theorem
> is proved in the current theory. It's perhaps easy to see how to work
> around that, e.g., by having a notion of "theory assumptions" that need
> to be discharged before the theory can be closed, or some such thing,
> but it's worth debating whether such an approach is necessary.
> 
> We already have a form of legible theories, produced by "print_theory"
> and "html_theory", so why is it important to have a theory syntax that
> the system accepts as input?

Why?  Simply because it makes the system more usable.  
I would suggest you sit down and use PVS for a while, and consider the
factors that make it substantially more usable than HOL.  One of these
is the way theories are no longer declared by step-by-step interactions
with a command line, but rather are declared using a reasonable
syntax in a single file.  

The rationale for the design decisions taken in PVS is well documented
in the "Prolegomena to the Design of PVS, IEEE Transactions on Software
Engineering, Vol 21, No 2, 1995".  It makes a good read, and though we
may not agree with everything there, there is alot that we 
can learn from.  Most of their arguments carry over directly into
the HOL/LCF world.

Regarding specifications: I think it is reasonable to expect that the
process of declaring a theory may require some theorem proving.  PVS
goes even further here, requiring theorem proving during type checking.
I don't think I'd suggest that, but theorem proving during
specification seems OK.  For instance your recursive function package
needs this, doesn't it Konrad?  So why not provide decent support
for managing proof obligations?  

Regarding managing proof obligations: In the average 
"requirements specs" for a formal methods systems, 
automatic management for proof obligations
is seen as essential.  It's obvious why: it allows users 
to explore properties of their specification without being required 
to discharge all obligations.  The fact that it may be hard to 
implement in HOL says alot more about the 
weakness of that system than it does about the usefulness of 
such a facility!  But in principle it should be possible to implement an
excellent proof obligation management mechanism on top of
an LCF core.  After all the security of an LCF system should give
us the freedom to implement sophisticated mechanisms, without
compromising the soundness of the system.

You contemplate modifying the existing theory mechanism.
IMHO, the current theory mechanism is a mess, and a first step
toward making progress would be to toss it away!
How about replacing it with two things:
	- storage primitives for theorems
	- an interface/management mechanism based around abstract theories
         and theory description files, with a decent interface based
         on Emacs or Tk.
The storage of theorems and the management of the user's workspace
are quite separate issues.  Theories in hol88 and hol90 are a good
example of how one mechanism can be used to try to solve too many problems!

Cheers,
Don.