Соображения по теме.

1. Учитель математики рассказывал нам такую историю. В начале 20 века группа математиков (м.б. Бурбаки, точно не помню) решила издавать журнал, в котором использовались бы только математические значки. Из тех соображений, что для записи доказательств их (значков) достаточно. Так вот - ничего не вышло. Никто не мог "читать" такой журнал. Слова обычного "нестрогого" языка необходимы для передачи мысли.

Также и в программировании. Читать гораздо труднее, чем писать. Строгость вторична по отношению к пониманию.

2. Все абстракции текут (С). Спольски достаточно об этом написал. Ещё мне нравится реальная история с алгоритмом быстрой сортировки в стандартной библиотеке Java. Гослинг лично признаётся в своих "грехах" - очень познавательно. С алгоритмом всё нормально. Проблема при его переносе на конкретную архитектуру вычислителя (JVM в данном случае).

То есть, что толку, что мы докажем абстрактную правильность программы. Она же выполняется в конкретном окружении, "просчитать" все состояния окружения невозможно.

3. Существует теорема о мёртвом коде. От этого никуда не деться. А это означает, что любые попытки строгой верификации ограничены в принципе.

Получается, что программирование - это больше искусство, чем наука. Математика, как база алгоритмизации, никуда не девается, но при практическом программировании на первый план выходят совсем другие вещи. Не случайно Ларри Уолл (автор Perl) и Бертран Мейер (автор Eiffel) подчёркивают, что при создании языков на них большое влияние оказывала лингвистика.

На современном этапе индустрия ПО пытается справляться со всеми этими проблемами путём создания специализированных языков: SQL для баз данных, R для статистики и т.п. Другое направление - это более-менее универсальные языки очень высокого уровня типа Python и Ruby. В любом случае количество математики для прикладного программиста имеет тенденцию к уменьшению.

iv_an_ruotziчто толку, что мы докажем абстрактную правильность программы.Разумеется, никакого толку. Точно так же, как любое безуспешное выполнение любого теста --- тоже деньги на ветер...Согласен. Я не говорю, что верификация не нужна ВООБЩЕ. Есть области, где она очень даже приветствуется, Вы уже их упоминали. Я говорю о том, что:
1) Её полезность зависит от прикладной области.
2) Её применение ограничено принципиально. Например тем, что проверить правильность поведения программы на бесконечном наборе пользовательского ввода помноженном на бесконечное число возможных состояний окружения, невозможно.

Мы ведь здесь говорим о прикладном программировании, не так ли? Если потеоретизировать, то это к знатокам Haskell, я пас. Тут уже упоминали Coq, например. Да, там взаимная польза математики и программирования очевидна. Пример удачной "прикладной" области. Но когда Вы пишете десктопное приложение с неформализованными и постоянно меняющимися требованиями заказчика - это совсем другая история. Вот об этом я говорю.