Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: Donald.Syme@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de
In-Reply-To: <E0tkbg9-0001aS-00@bescot.cl.cam.ac.uk> (message from Donald Syme on Thu, 8 Feb 1996 19:06:37 +0100)
Subject: Re: hol90 should have more control about proofs
Message-Id: <96Feb12.010012met.8161@sunbroy14.informatik.tu-muenchen.de>
Date: 	Mon, 12 Feb 1996 01:00:06 +0100


Don:
> 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?

Ralph:
> Teaching the use of hol to students, I always ran into questionsmarks
> on top of their bodies instead into heads...  learning a programming
> language to USE hol and to ENHANCE hol at the same time has sooo
> confused the people, especially when for novice students, there is no
> obvious difference between sml and hol at the first time.

Well, that's a good point. Still, I am interested in bringing the two
languages closer together, as in LAMBDA. Maybe if we all bought colour
workstations and the HOL was coloured blue and the SML was red?

Konrad.