Цена ошибки (в коде)⁠⁠

Из учебного пособия А.С. Камкина "Введение в формальные методы верификации программ"

В 1982 г. канадской фирмой Atomic Energy of Canada Limited был запущен в серию

медицинский аппарат «Therac-25», предназначенный для лучевой терапии — облучения раковой опухоли. В «редких» ситуациях из-за ряда ошибок, допущенных при

проектировании и реализации встроенной системы управления, интенсивность облучения возрастала на 2 порядка и более. За время эксплуатации прибора (период

с июня 1985 г. по январь 1987 г.) как минимум два пациента умерли, а несколько

человек остались инвалидами...

23 марта 2003 г. во время войны в Ираке американский зенитно-ракетный комплекс

«Patriot» ошибочно идентифицировал британский бомбардировщик «Tornado», летевший близ кувейтской границы, как приближающуюся вражескую ракету и автоматически произвел залп. Погибли два пилота. Спустя полторы недели, 2 апреля,

«дружественным огнем» был уничтожен американский палубный истребитель-бомбардировщик F/A-18 «Hornet». Еще один пилот погиб.