Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Tue, 24 May 1994 22:00:01 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199405241200.WAA04034@achernar.anu.edu.au>
To: hol2000@leopard.cs.byu.edu
Subject: Re: hol2000 is very silent


Ralph:    I myself am not very encouraged to switch to another new hol

Matthew:  ... one should be able to postulate theorem and then pick and choose
          between `proof engines'  -- rather than spend hours, days or months ....
          So, that's a wish.

Richard:  ... development of hol90 will, I hope, continue.

Ralph is right to expect effort in conversion but is he doing his accounting
correctly?  He should be offsetting the costs with savings he might make from
faster proofs in the years 2002 - 2010, say.  (He'll probably have to convert
again every decade.  "No Pain - No Gain" seems to be a fact of life if you stay
at or near the cutting edge.)   Even with a much less dramatic vision than
Matthew's its not hard to imagine that big improvements in productivity might
result from redesign of HOL.   We could then have Ralph saying again in 2005,
  "IMHO, it was worth it, but ...".


There's a sense in which  hol2000@leopard  will be a forum for wish-listing but
the benefits of each new idea should be assessed in the twin contexts of;
	a) extensions or modifications to HOL90;
	b) implementation in the evolving HOL2000 theorem proving environment
	   (as it stands at the time).
If every significant suggestion turns out to be implementable perfectly well
in HOL90 then HOL2000 will never happen.   Could it then be said that HOL90
(or HOL90++) has been PROVEN to be the optimal system?  or would it be said
that the HOL community lacks the wit and vision to track the state-of-the-art?

A danger in having discussions about abandoning HOL90 in 2004 (or whenever) is
that we might inhibit activity on its development right now.  My view is that
the hope of HOL proofs being less painful in a HOL2000 will INSPIRE the
development of theories, tactics, decision prcedures and tools, and that will
improve HOL90 in the interim.  (Any software product that serves as a
workhorse for a decade is a total success, and concern about the investment
being discarded at that time is misplaced.)

If, on the other hand, we don't talk about where we are going, Ralph may find
he has to convert again, anyway, because the HOL enterprise is defunct.  In
that case it might be even more pain.

Malcolm Newey