Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 23 Jun 1993 12:32:26 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06207; Wed, 23 Jun 93 04:23:45 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA06202; Wed, 23 Jun 93 04:23:39 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 23 Jun 1993 12:22:28 +0100 To: info-hol@ted.cs.uidaho.edu Subject: Discussion of hol90 In-Reply-To: Your message of "Tue, 22 Jun 93 21:34:45 PDT." <9306230434.AA17035@maui.cs.ucla.edu> Date: Wed, 23 Jun 93 12:22:24 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:039570:930623112232"@cl.cam.ac.uk> It should "in principle" be easy to translate automatically from Classic ML to SML -- it's just a matter of someone actually bothering to write a translator. There are a few semantic differences (e.g. tuples in Classic ML are iterated pairs, whereas in SML they aren't). I believe there are moves afoot in certain quarters to produce a version of ML which is not tied to a particular concrete syntax, but lets users produce their own bespoke versions. There is an obvious danger (people may be unable to communicate with each other), but it could provide a simple solution to the problem of porting code between Classic ML, SML and CAML. It would be useful if Konrad's work on embedded syntax could be included in such a generalization. I would prefer to use hol90 under CAML (I have trouble overcoming my revulsion for SML's "let .. val .. fun .. end" syntactic atrocities despite learning SML three years before Classic ML), but I think we should really concentrate on the further development of hol90 itself. One of the reasons HOL has been more highly developed than other theorem provers is that people just use it despite its shortcomings, developing real experience of the problems, rather than endlessly refine the fundamentals in response to frequently short-sighted and misconceived whinges. John.