Я немного читал об этом, но есть две проблемы.
Во-первых, вы не можете доказать какую-то абстрактную вещь, называемую правильностью. Вы можете, если все настроено правильно, доказать, что две формальные системы эквивалентны. Вы можете доказать, что программа реализует набор спецификаций, и это проще всего сделать, построив доказательство и программу более или менее параллельно. Следовательно, спецификации должны быть достаточно подробными, чтобы предоставить что-то, с чем можно столкнуться, и , следовательно, спецификация фактически является программой . Проблема написания программы для достижения цели становится проблемой написания формальной подробной спецификации программы для достижения цели, и это не обязательно шаг вперед.
Во-вторых, программы сложные. Так же как и доказательства правильности. Если вы можете ошибиться при написании программы, вы можете сделать одно доказательство. Дейкстра и Грис, по сути, сказали мне, что если бы я был идеальным математиком, я мог бы быть хорошим программистом. Ценность здесь в том, что доказательство и программирование - это два несколько разных мыслительных процесса, и, по крайней мере, по моему опыту, я совершаю разные ошибки.
По моему опыту, проверочные программы не бесполезны. Когда я пытаюсь сделать что-то, что я могу описать формально, проверка правильности реализации устраняет множество трудно обнаруживаемых ошибок, в первую очередь оставляя тупые ошибки, которые я легко обнаруживаю при тестировании. В проекте, который должен генерировать чрезвычайно безошибочный код, это может быть полезным дополнением. Это не подходит для каждого применения, и это, конечно, не серебряная пуля.