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

[John Nagle]

Paul Rubin wrote:
> Kay Schluehr <kay.schluehr at gmx.net> 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: "http://citeseer.ist.psu.edu/53148.html"

	Square root: "http://portal.acm.org/citation.cfm?id=607571"

A longer paper:

	http://www.computationallogic.com/news/amd.html

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

					John Nagle