Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
To: Paul.Loewenstein@Eng.Sun.COM (Paul Loewenstein)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: HOL90 is faster, for me
In-Reply-To: Your message of "Mon, 21 Jun 93 21:01:23 PDT." <9306220401.AA04736@lara.Eng.Sun.COM>
Date: Tue, 22 Jun 93 11:05:08 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:125300:930622100518"@cl.cam.ac.uk>

I don't disagree with the arguments for moving to HOL90, but before we kill
HOL88 stone-dead, there are some points that I have, or that have been made to
me in the past, which are worth stating:

1. HOL88 can be used on (what are now) low performance machines, e.g. Sun3 with
   8 Mbytes; HOL90 requires LOTS of memory to perform effectively.

2. HOL90 is not as mature as HOL88, and in my opinion has only recently become
   mature enough for serious use. However, HOL90 is still a lot less stable
   than HOL88. One thing that users have complained about in the past is major
   changes to the system and new releases every few months.

3. Projects which started a year or two ago may be using HOL88, so we should
   continue to support HOL88 (at least minimally) until those projects have
   been completed.

4. HOL88 requires a Lisp interpreter/compiler. HOL90 requires Standard ML.
   I believe that Lisp is much more widely supported than Standard ML (correct
   me if I'm wrong), so HOL is, in some sense, in safer hands with Lisp.
   Is Standard ML going to flourish? Or will it die because of Lisp, Haskell
   or some other language? (I'm not trying to put SML down --- I like it, but
   can someone `in the know' comment on just how widely used SML is?)
   Of course, we can look at it the other way and say that Standard ML has a
   much better chance with the HOL community using and supporting it!
   We are however in danger of putting all our eggs in the SML of New Jersey
   basket.

There are probably other issues that I've missed. My feeling is that HOL90 is
now mature enough, and that high performance machines with large enough
memories are common. So, perhaps it is time to make HOL90 the standard and put
all our weight behind it?

Richard Boulton
University of Cambridge Computer Laboratory