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: Discussion on meta-language for HOL
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Fri, 25 Aug 1995 09:10:57 +0200
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.782:25.08.95.07.15.18"@ira.uka.de>

> 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.
> 
> Can we bring 2./3. and 4. together means can we combine C-like languages
> and functional languages together, fullfilling 2.)-4) at the same time
> with the same quality? IMHO, you can't have it both ways. 
> 
> a) Choosing something like ML, LISP,... (just note that there is not ONE 
> language here) means problems with 2.) or 3.) or both.
> 
> b) Choosing C means problems with 4.)
> 
> c) Using a compromise by mulating the meta-language like ML in C means
> problems with 3.)
> 
> Personally, I think there are two options:
> 
> A) You want to use theorem provers as a research thing only. Then you
> think 4.) is that important, that you skip 2.)/3.) and choose a)
> 
> B) You want to use theorem provers in `real-world applications', too. You
> want to make theorem provers persisting much longer that one or two
> generations of researchers. Then 2.) and 3.) is so much important, that
> you may use c) only as a transitional state (something like being
> `MS-DOS compatible' ;-) to finally get b).
> 
> In my point of view, you finally have to choose between A) and B). If
> you don't really choose, that will mean you have chosen A). Do your
> choice :-). Endless discussions will make users running away from theorem
> provers because nobody wants to build his house(even not his/her p.h.D. topic)
> on a very uncertain base.
> 
> :-) 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                                        *)
> (*                                                                 *)
> (*******************************************************************)