Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sun, 7 Mar 1993 07:17:26 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11287; Sat, 6 Mar 93 23:02:14 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA11282; Sat, 6 Mar 93 23:02:08 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA05638; Sat, 6 Mar 93 23:01:48 -0800 Message-Id: <9303070701.AA05638@maui.cs.ucla.edu> To: mel@EDU.CORNELL.EE.ultrastar (Miriam Leeser) Subject: Re: Constructive logic, Nuprl and Hardware Verification Cc: info-hol@edu.uidaho.cs.ted Date: Sat, 06 Mar 93 23:01:47 PST From: chou@edu.ucla.cs Not being an expert in hardware verification or Nuprl, I have a naive question. I got the impression that as far as hardware verification is concerned, all the advantages one gets in using Nuprl as opposed to HOL are in the more powerful type theory of Nuprl. The constructivity of Nuprl seems to be only a distraction that has little to do with hardware verification. Is this impression correct? Personally I suspect few hardware engineers (or mathematicians, for that matter) doubt the soundness of classical reasoning. - Ching Tsun