Kay Schluehr <[EMAIL PROTECTED]> 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. -- http://mail.python.org/mailman/listinfo/python-list
