С точностью до значащих разрядов?
Интересно бы послушать эту часть формального доказательства. Программист видимо действительно был достаточно толковый и помнил не только уроки арифметики, но и уроки программирования :-))

Забавно, но больше всего как раз запомнилось, как года 3 - 4 назад я пострал от "математиков" в программировании. Пытался я тогда купить через интернет билеты у одной маленькой карибской авиакомпании. После долгого и нудного заполнения четырех экранов с кучей полей я наконец добрался по последнего, с заветной кнопкой "купить". Облегченно вздохнув, нажимаю эту кнопку. А они мне говорят - пока вы тут думали, цена билетов изменилась типа с 157.35 на 157.35, если вас новая цена устраивает - жмите кнопку "купить". Ну всяк бывает - на этот раз не долго думая жму кнопку, а они мне в ответ пишут опять про новую цену. Раз на 5ый я уже смирился с необходимостью звонить и покупать билеты по телефону, но решил посмотреть на код выдаваемой страницы -а там, в java script, достаточно быстро нашлась та самая проверка на равенство: a*(b + c) == a*b + a*c.