В книге "Дисциплина программирования" (1976) Э. Дейкстра пишет "Даже в случае полностью детерминированных машин полезность тестирования программ оказывается сомнительной. Тестирование программы может вполне эффективно служить для демонстрации наличия в ней ошибок, но, к сожалению, непригодно для доказательства их остуствия". Далее Дейкстра развивает подход, в котором операторы языка рассматриваются как преобразователи предикатов, а верность программы можно доказать математически с помощью формальной логики.

Какой статус сегодня? Из конференций (например, Разработка ПО) следует, что тестированию отводится существенная роль, хотя возникающие проблемы в многопоточных и распределенных системах (массовый пример - онлайн игры) требуют все более изощренных приемов. Традиционный подход к тестированию заключает в том, что тесты должны покрывать все строки кода (то есть реализовывать переходы во все условные блоки. Как указал Дейкстра, выполнение каждой строки кода не гарантирует правильность алгоритма - правильность была бы доказана, если бы программа выполнилась с правильным результатом при всех наборах внешних условий - возможность такой проверки делает бессмысленной существование самой программы. Нередка ситуация, когда многопоточное приложение отладить нельзя и его выкидывают на помойку и переписывают заново, что негативно сказывается на сроки выпуска продукта и доходы попавших в такую ситуацию компаний.

Есть ли прогресс в рамках математического подхода доказательства корректности программ? Какие-то новые книги, учебные курсы, программные средства?