Return-Path: 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 15:52:02 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA085751012; Fri, 25 Aug 1995 08:30:12 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA085560909; Fri, 25 Aug 1995 08:28:29 -0600 Received: from mallard.cl.cam.ac.uk (user adg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 25 Aug 1995 15:27:55 +0100 To: Donald Syme Cc: hol2000@leopard.cs.byu.edu Subject: Re: Discussion on meta-language for HOL In-Reply-To: Your message of "Fri, 25 Aug 1995 12:58:03 BST." <"swan.cl.cam.:250290:950825115808"@cl.cam.ac.uk> Date: Fri, 25 Aug 1995 15:27:46 +0100 From: Andrew Gordon Message-Id: <"swan.cl.cam.:019670:950825142916"@cl.cam.ac.uk> Don wrote: >BTW, perhaps Andy Gordon could give us the run down on whether >Miranda would be practical to use for a theorem prover?? I agree that ML is the solution in the short-medium term. I've never heard anyone criticise an ML-based prover on the grounds that it wasn't written in a lazy language like Miranda or Haskell. Since compilers for lazy languages are famously slower than ML compilers what point would there be in going over to Miranda or Haskell? Andy.