Charles D Hixson wrote:
An excellent warning on proofs of correctness is at:
http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
Hear, hear.
But I don't take away the lesson that "not even formal methods are
powerful enough". They would've caught this if, for example, they'd
assumed and proven from transistor diagrams of the underlying chip.
Formal methods break when their axioms break, and the proof of
correctness for this code presumably used axioms that were only true
most of the time, axioms that could be broken even without cosmic rays.
I don't think this is mere argument-in-hindsight; it occurred to me long
ago not to trust integer addition, just transistors. And even then,
shielded hardware and reproducible software would not be out of order.
--
Eliezer S. Yudkowsky http://singinst.org/
Research Fellow, Singularity Institute for Artificial Intelligence
-------
To unsubscribe, change your address, or temporarily deactivate your subscription,
please go to http://v2.listbox.com/member/[EMAIL PROTECTED]
