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; Thu, 24 Aug 1995 17:54:25 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA021221912; Thu, 24 Aug 1995 10:31:52 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from bobcat.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA021191910; Thu, 24 Aug 1995 10:31:51 -0600 Received: from cs.byu.edu (localhost) by bobcat.cs.byu.edu (1.37.109.15/CS-Client) id AA005052119; Thu, 24 Aug 1995 10:35:19 -0600 Message-Id: <199508241635.AA005052119@bobcat.cs.byu.edu> To: hol2000@cs.byu.edu Subject: OK, so what about something based on C? Date: Thu, 24 Aug 1995 10:35:18 -0600 From: Phil Windley I think SML/nj dependence for hol90 is a major weakness. This is my biased opinion since I've never been able to run it due to the inability to get SML/nj working on HPPA (HP's). Nevertheless, I think it points out a weakness of hol90 vis 'a vis hol88. Because hol88 is based on LISP and LISP is almost universally available, so is hol88. While I hate the thoughts of actually doing it, why not define the meta language (something like Classic ML with the nice features of SML such as records) and then write it in C? Make it portable from the start. This is a lot of thankless work, but it provides the most portable implementation of HOL possible. --phil--