Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: murthy@cs.cornell.edu, info-hol@leopard.cs.byu.edu
In-Reply-To: <9411021735.AA26727@deneb.cs.cornell.edu> (message from Chet Murthy on Wed, 2 Nov 1994 18:35:14 +0100)
Subject: Re: bhogan@bedlam: HOL90 on a PC
Message-Id: <94Nov3.100322met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 3 Nov 1994 10:03:08 +0100


> Why not try to port it to caml-light?  I mean, caml-light will soon
> have a functor-style module system, and it already has separate
> compilation (so if you only instanciate functors a few times, you can
> do it with cp/sed).  There is a *fantastic* package for writing
> parsers and pretty-printers which is *small*.  And there's work in the
> CAML group on syntactic extension in the style of the old CAML
> toplevel -- much more powerful than anything else available.


Yes! But it doesn't make sense to do ad-hoc ports: the right thing to do
is develop a portable HOL, and then port that. (Note that a portable
system should be more self-contained and therefore less apt to use
*fantastic* new goodies (or even ML-Yacc).) Probably the most portable
system would be implemented purely in the SML Core language, (maybe plus
structures to give separate namespaces).


> MoSML, sorry to say, would be a step backwards.  

That may be true, in some areas, but its concrete syntax is a winner in
regards to portability: a HOL system written in the SML Core language has
lots of implementations to choose from. It would be a relatively simple
chore to translate to Caml-light.

Of course, nobody wants to have to translate: it's a job that is never
done. This situation shows how HOL users have to pay for the inability
of the ML community to agree on a single concrete syntax back in the
heady days of designing Standard ML. I hope that the ML2000 initiative,
among its grand aims, includes the humble one of syntactic rapprochement
with the CAML crowd.

HOL2000/QED thought: could agreement on a concrete (or abstract) syntax
for the term language happen for the large number of HOL-like theorem
provers?

Konrad.