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

[Paul Rubin]

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.

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.