Return-Path: Return-Path: Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP to fgate (PP) id <20991-0@swan.cl.cam.ac.uk>; Fri, 29 Mar 1991 19:44:02 +0000 Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk with SMTP inbound id <15853-3@sun2.nsfnet-relay.ac.uk>; Fri, 29 Mar 1991 19:41:35 +0000 Received: from iris.ucdavis.edu by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP id aa10404; 29 Mar 91 19:08 GMT Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.4.0) id AA02978; Fri, 29 Mar 91 11:32:47 -0800 Received: from cs.ubc.ca by clover.eecs.ucdavis.edu (5.59/UCD.EECS.1.11) id AA21838; Fri, 29 Mar 91 11:33:59 PST Received: by cs.ubc.ca (4.1/1.14) id AA25621; Fri, 29 Mar 91 11:32:32 PST Date: 29 Mar 91 19:33 From: Jeffrey Joyce To: info-hol@edu.ucdavis.clover Message-Id: <1749*joyce@cs.ubc.ca> Subject: "why h.o.l. ?" At the hol user's group meeting last October in Aarhus I gave a talk which suggested two reasons why one might justify the use of higher-order logic for hardware spec/verf (these were "generic specification" and "embedded formalisms"). I'd be very interested to hear suggestions from others on how one might justify the use of higher-order logic over less expressive formalisms such as first-order logic. I'm not really interested here in the question "why (or why not) use the HOL system ?" (which is a very different question). I am really just interested in the formalism itself (i.e. higher-order logic). Any suggestions ? - Jeff