Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <199405240813.AA02815@borneo.gmd.de>
To: hol2000@leopard.cs.byu.edu
From: Matthew Morley <morley@gmd.de>
Subject: Re: hol2000 is very silent
In-Reply-To: Your message of "Tue, 24 May 94 09:13:24 EDT." <"i80fs2.ira.732:24.04.94.07.13.27"@ira.uka.de>
Date: Tue, 24 May 94 10:13:52 +0200

Ralf says:

-I myself switched from hol88 to hol90 with
-a LOT of work. Everything from programs, proofs,
-lectures for students to documentation had to
-be changed. IMHO is was worth, but it shows a
-problem with hol2000: 

Yaeh, yeah, we know, we know! But my impression is
that this should be more a wish list than an agony
column!

Think of the positive benefits a real theorem
proving environment could bring. Doesn't this just
emphasise the point Peter Andrews raised at last
year's HUG about portability of proofs and
theorems and developing interfaces between tools?
I didn't get the impression at the time that
HOLers took that discussion very seriously, but in
my opinion (it's just that) this ought to be if
not at the forefront at least in the vanguard of
any future initiatives in the development of
theorem proving technology. In time one should be
able to postulate theorem and then pick and choose
between `proof engines' (or even not care which is
used) -- rather than spend hours, days or months
trying to figure out how to *express* the idea in
HOL, Isabelle, PVS, TPS, Lambda, Nuprl, Larch....

So, that's a wish. Obviously this entails (upward)
compatability as Ralf desires, as long as HOL has
the right back-end. But unless ML2000 is upwardly
compatible with SML then one can't really expect
programs to port. (NB. A proof in HOL is *not*
REAPEAT GEN_TAC THENL [...]).

OK, enough nonsense form me.

M