Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 25 Aug 1995 17:09:04 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA082927356;
          Fri, 25 Aug 1995 07:29:16 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA082427257;
          Fri, 25 Aug 1995 07:27:37 -0600
Received: from ira.uka.de (actually i80s16.ira.uka.de) by iraun1.ira.uka.de 
          with SMTP (PP); Fri, 25 Aug 1995 15:17:37 +0200
X-Mailer: exmh version 1.5.3 12/28/94
To: hol2000@leopard.cs.byu.edu
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Fri, 25 Aug 1995 15:14:48 +0200
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.424:25.08.95.13.17.39"@ira.uka.de>


I agree that in the short run, sticking to ML may be the easier way.
It would be great to have HOL90 running under CAML,SMLNJ and MoscowSML at
the same time. But just one note: MoscowSML, e.g., has no elaborate
module system, especially functors are missing. That leads to real mayor
changes in HOL90 and these changes are not only internally (just think
of the library "mutrec", with uses functors) but also for the user.
I don't know what the state of CAML is. People had already a lot of
stress in transfering from HOL88 to HOL90 and in fact, there suppose to
be people out there who did not switch. Remember when in 
HOL90.4 (I guess it was 4), the syntax changes to records. That was another
mayor change, causing reprogramming. Making HOL90.8 running under these
different ML dialects will again start this reprogramming. And what about
HOL90.X under SML Y? How often will we have to reprogram the same stuff?
I'm not very hilarious about doing that again and again...one should be
very careful with mayor changes. We may reach a point there nobody wants
to reprogram his old stuff again to make it running with the newest
version of HOL90 and then, we will have a serious problem.

Ralf.


(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  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 6083771                                        *)
(*                                                                 *)
(*******************************************************************)