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

Ну я согласен в том, что доказательство программ синергирует с генерацией программ. Это действительно так и есть даже фундаментальный результат, что по конструктивному доказательству спецификации можно сгенерировать программу, ее реализующую. Но вот с классическим программированием идет война - как сам Хоар говорит, тестирование конфликтует с верификацией.