Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Cc: reetz@ira.uka.de, donald.syme@cl.cam.ac.uk
Subject: RE2: hol90 should have more control about proofs
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Fri, 09 Feb 1996 11:04:17 +0100
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.536:09.02.96.10.05.07"@ira.uka.de>

>The word "proof" is severely overloaded.  I want to make clear that
>in this context we're not talking about "proof objects" 
>i.e. low level representations of the sequence of 
>deductions that lead to a theorem.  Instead I am interested
>in the proof as the user enters it, i.e. the

Yes, that's exactly what I have had in mind. "more control about
proofs" is aimed at the useability of HOL.
types, terms, constants, definition, theorems AND proofs should
be considered as some sort of "objects" stored in a special form
of a database and we do need simpler, easier posibilities of
>visualizing< and >maintaining< ont only these objects, but also
their >dependencies< to each other in order to give the user
a better understanding of what the current state of his work with HOL is.
As virtual theories is a very elegant way for >maintaining< certain
dependencies, the database query language from Gunter or xholhelp is an
approach for >visualizing< it. In the long run, we need a combination
of both in one, unique "metaphor" unifying >visualizing< and >maintaining<
like e.g. the "desktop" in Apple OS or Windows95. I still have no idea about 
what the fitting "metaphor" should be. a first sort of "gimmick" I was
experiencing with was using graphs as metaphor with the graph visualization
system daVinci. However, this is still "to much low level" and I ran into that 
missing >maintaining< facilities of the current HOL90, starting this
discussion here.

>So, in the long run I believe it would be better to 
>clearly distinguish between user interaction languages and the 
>implementation language. 

Yes and Yes and Yes! 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. I believe that we should make a difference between
experts, who do program new decision procedures at the implementation
level for efficiency reasons and users, who mainly use hol and
temporarly write some small tactics. hol users should have a 4th
Generation language (like Delphi?), which is much more abstract than sml
and much closer to the things the user may want to "program" (I did use
quotes here intentionally).
[Once we have made that difference, we can do one of my ""favorite""
discussions again: sml version C as implementation language of a hol system ;-]

Ralf


(*********************************************************************)
(*                                                                   *)
(*  Ralf Reetz                                                       *)
(*  Research Assistent                                               *)
(*  Sonderforschungsbereich 358 der deutschen Forschungsgemeinschaft *)
(*  "Automatisierter Systementwurf"                                  *)
(*  University of Karlsruhe                                          *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                  *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany                *)
(*                                                                   *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de    *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html         *)
(*  fax:    +49 721 370455                                           *)
(*  tel:    +49 721 6084220                                          *)
(*                                                                   *)
(*********************************************************************)