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; Tue, 24 May 1994 20:01:27 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA05568; Tue, 24 May 1994 12:58:39 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from localhost by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA05564; Tue, 24 May 1994 12:58:38 -0600 To: hol2000@leopard.cs.byu.edu Subject: A better user interface Date: Tue, 24 May 1994 12:58:38 -0600 From: Kelly Hall Message-ID: <"swan.cl.cam.:102720:940524190201"@cl.cam.ac.uk> Over the last year or so I've helped several students learn HOL, and more than a new metalanguage or an enhanced logic I think we need a better user interface. After a few months using PVS, I loathed going back to HOL. I find it much easier to use the PVS/Emacs interface because: a) the goals and assumptions are presented clearly. b) numbering assumptions and using their index in rewrite rules is easier than FIRST_ASSUM and ASSUM_LIST, although it makes a proof more 'brittle'. c) The LaTeX support for proofs and source files is convenient. While I think it's great that the HOL community has learned to tolerate the existing interface, I think if we want HOL to spread to industry we'll have to make it easier to use. I think it's possible to create a PVS-like interface for HOL while retaining backward compatibility with the existing HOL/Emacs interface. It just requires a smarter interface, not a smarter HOL. It might be nice to experiment with something besides Emacs, though. Maybe tcl/tk or something similar. Kelly