PEP 3107 and stronger typing (note: probably a newbie question)

John Nagle nagle at
Sat Jul 21 20:43:11 CEST 2007

Paul Rubin wrote:
> Kay Schluehr <kay.schluehr at> writes:
>>When I remember correctly the FDIV bug was due to a wrongly filled
>>lookup table and occurred only for certain bitpattern in the divisor.
>>I'm not sure how a formal proof on the structure of the algorithm
>>could help here? Intel repaired the table i.e. the data not the
>>algorithm that acted upon it.

    No, Intel had assumed a symmetry that wasn't actually true.

> I would expect the table contents to be part of the stuff being
> proved.  I hear that they do use formal proofs for their floating
> point stuff now, as does AMD.  AMD apparently uses ACL2 (a theorem
> prover written in Common Lisp, info about AMD is from the ACL2 web
> site) but I don't know what Intel uses.  I've figured that the FDIV
> problem was one of the motivations for this but I'm not certain of it.

     Yes, here's two of the papers describing proofs of AMD
floating point unit correctness.

	Division: ""

	Square root: ""

A longer paper:

This stuff is hard to do, but notice that AMD hasn't had any recalls
for floating point problems.

					John Nagle

More information about the Python-list mailing list