Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 26 May 94 12:41:10 EDT
From: reetz <reetz@ira.uka.de>
To: hol2000@leopard.cs.byu.edu
Subject: User interface versus expanding the logic
Message-Id: <"i80fs2.ira.481:26.04.94.10.41.14"@ira.uka.de>

david shepherd said:

>Perhaps one of the things that hol2000 should have in mind is that it
>would be the theorem prover core of a system with a (or perhaps a
>variety of) user interface on top.

I personally do agree to that point of view. I would even like to say it
a little bit provocative:

do we need hol2000 or do we need a better user interface of an existing hol ?

In my point of view, we do need a better user interface and more
specialized proving facilities ON TOP of an existing hol. Take e.g.
ARITH_CONV: we might like to have something similar for ==`:integer`==,
==`:list`==, an so on. Take e.g. the subgoal package: we might like to
have a graphical representation, too (in the 20th subgoal after
35 different cases, the anonymous hol user might ask: where the hell I am now?).
Take e.g. deep embedding of new languages: we might like to have something
which automates e.g. syntax embedding (look at compiler compilers: a lot
has been automated). We might like to have more complex data types:
beside things like ==`:num`== or ==`:word`==, we might like to have
arbitrary dimensional arrays, record, stacks, queues, whatever (but
with as much as automated proving facilities as possible!).
Another point: If I'm looking for let's say the wonder thing "X", then
people suggest: no problem, take hol system "A". But then I'm looking for
let's say the wonder thing "Y", then people suggest: no problem, take
hol system "B". If we were able to ``merge'' all these existing things
into one system, we would already win a lot (that's a bunch of work, 
I know :-(

In my point of view, what hol makes so hard to deal with is the plenty
of time I need to formalise or even prove ``trivial'' things. We are
still on the ``machine language level'' (I'm sorry, if I might sound 
too frustated :-{.

Or let me put it in that way: what are the applications of hol and
what does these applications need? Consider e.g. the following
(certainly far, far away from being complete) division into two
different ``worlds'':

- formal verification of hardware/software:
  That's a topic for industrial applications.
  In my point of view, here we are still on the machine language level
  in too much cases. See suggestions above.
  
- mechanising new ``mathematical theories'':
  That's a topic for university applications.
  here, IMHO hol already offers a lot: the different mechanisms of
  automated type definitions. We might like to have more syntactical
  stuff (I'm truly sorry for ``syntactical stuff'', I don't know a better 
  word right now)
  like dependent types, something like constrained logic programming ?,
  and other things as already discussed here.


hope this provokes more discussions ;-) 
Ralf.