PEP 3107 and stronger typing (note: probably a newbie question)
nagle at animats.com
Sat Jul 21 20:43:11 CEST 2007
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.
Square root: "http://portal.acm.org/citation.cfm?id=607571"
A longer paper:
This stuff is hard to do, but notice that AMD hasn't had any recalls
for floating point problems.
More information about the Python-list