From owner-qed Tue Nov 29 10:10:47 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA13742 for qed-out; Tue, 29 Nov 1994 10:05:03 -0600 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id KAA13732 for ; Tue, 29 Nov 1994 10:04:53 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 29 Nov 1994 16:04:14 +0000 To: info-hol@leopard.cs.byu.edu, qed@mcs.anl.gov Subject: Re: FWD: NYTimes article on Pentium bug In-reply-to: Your message of "Sun, 27 Nov 1994 11:54:31 PST." <9411271954.AA06250@maui.cs.ucla.edu> Date: Tue, 29 Nov 1994 16:04:03 +0000 From: John Harrison Message-ID: <"swan.cl.cam.:297130:941129160419"@cl.cam.ac.uk> Sender: owner-qed@mcs.anl.gov Precedence: bulk I'm curious about whether the problem was in the underlying algorithm used or its hardware implementation. If I interpret the press report correctly: | Intel said the error occurred because of an omission in the translation of | a formula into computer hardware. It was corrected by adding several dozen | transistors to the chip. the error arose in transcription at some stage. Is that right? Perhaps I read too much into journalese. But if so, it may be that formal verification wouldn't have helped unless it was very tightly coupled with the production process. Nevertheless, I believe floating point hardware is a particularly good target for formal verification by theorem proving. Providing the necessary mathematical infrastructure for such verification efforts was the motivation for all my work on formalizing analysis in HOL (though it has since become an interest in itself). John.