Без заголовка

Ребята из ERTOS потратили 2 человеко-года на написание Haskell-прототипа, и 2 человеко-месяца на переписывание его на С. И затем грохнули 20 человеко-лет на доказательство правильности кода -- 11 человеко-лет на само доказательство и 9 человеко-лет на инструментарий для этого доказательства. Т.е. стоимость "доказанного кода" идет к стоимости "недоказанного кода" примерно как 10:1). А вот тут они не совсем передовые, потому как последние достижения позволяют говорить о том, что оверхед для верификации будет небольшой, сравнимым с размером кода. Правда, надо использовать специальные наработки. Тут тоже своя инженерия есть - инженерия доказательств :).