Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
To: hol2000@leopard.cs.byu.edu
Subject: Re: Discussion on meta-language for HOL
In-Reply-To: Your message of "Fri, 25 Aug 1995 09:10:57 +0200." <"iraun1.ira.782:25.08.95.07.15.18"@ira.uka.de>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Fri, 25 Aug 1995 12:58:03 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:250290:950825115808"@cl.cam.ac.uk>

> > To summarize, to me, it looks like the HOL community
> > 
> > 1.) Can't agree on what meta-language one should use for theorem provers
> >     because of
> > 
> > 2.) Portability and
> > 
> > 3.) Effiziency and
> > 
> > 4.) Programming style
> > 
> > In my point of view, the only solution for 2.) and 3.) with industry-quality
> > solution is, like it or not, C or even harder, C++.
> > However, the solution for 4.) is something like ML, SML, CAML, LISP or
> > whatever functional, so the meta-language is close to the logic.

In the short-medium term,  I think the solution 
is simple - stick with ML, and make sure hol90/hol2000 
compile under PolyML, MoscowML and NJSML.  Work hard on making
the code tight and efficient.  Don't use any system 
dependent features that can't be duplicated in these
other systems.  I will be pushing for hol90.8 to be released
in a state ready for use with these different MLs, and will
offer to do the work to ensure this is the case.  (I know
it's sad, but I'm still actually enjoy this sort of programming).

I should point out that C++ is often non-portable - e.g. getting
templates to compile using several different compilers is a
nightmare (I spent a year programming with this constraint).  Also,
the C++ implementations for UNIX systems are pretty bad.  I was
using cfront and g++ back in 93 - perhaps things have improved since then.  
g++ didn't do templates "properly" back then (has this changed??).  
As for exceptions, forget it.  The PC C++ compilers are much better.

Also, even C code isn't always so portable - look at the headers and
installation procedures for the GNU products and Tk/Tcl and
check out at the number of system specific things the implementors
have to be aware of before beginning their compilations.

But even then, C/C++ doesn't always end up so efficient!  For instance,
Tk/Tcl programs, written in one of the least efficient languages
around, frequently out perform C/C++/Motif programs, and are
much easier to write as well.  I think an ML implementation
of HOL can theoretically achieve far more data sharing and
perform more efficient garbage collection than a C implementation.  (Given
that, I'm just astounded at how much memory SMLNJ uses up...)

BTW, perhaps Andy Gordon could give us the run down on whether 
Miranda would be practical to use for a theorem prover??

Don Syme


-----------------------------------------------------------------------------
At the lab:							     At home:
The Computer Laboratory                                          Trinity Hall
New Museums Site                                                      CB2 1TJ
University of Cambridge                                         Cambridge, UK
CB2 3QG, Cambridge, UK
Ph: +44 (0) 1223 334688				      Ph: +44 (0) 1223 302521
http://www.cl.cam.ac.uk/users/drs1004/     
email: Donald.Syme@cl.cam.ac.uk
-----------------------------------------------------------------------------