[spoiler]В ближайшие пять лет появятся яркие примеры крупных проектов, реализованных подходом correct-by-construction, а также приложения верификации для особо критичных проектов: это коснется и минималистичного микроядра seL4 (это наверное единственная на сегодня платформа виртуализации, корректность которой доказана математически http://www.opennet.ru/opennews/art.shtml?num=23011 ), и безопасного программного стека SAFE, спонсируемого военным агентством передовых исследований США DARPA под собственный проект CRASH http://www.crash-safe.org , и проектировщиков Intel, и разработчиков протоколов для распределенных вычислений, прежде всего облачных...
Причина этой волны прозаична -- экономическая эффективность. Но при этом подобные наработки пока остаются в научных и производственных лабораториях, и даже в ближайшие 10 лет подобные подходы не статут мэйнстримом -- слишком высок порог входа. Главные заказчики подобных проектов сегодня -- это силовые структуры, непрерывно участвующие в эпических кибервойнах. Так, самый мощный на сегодня вирус stuxnet, атаковавший ядерные объекты, был выявлен и побежден лишь потому, что в нем оказался баг -- а вот если бы он был построен математически корректно (что сегодня вполне возможно), возможно, мы никогда о нем и не узнали (а сколько таких боевых вирусов действует незамеченными, или ждут команды для атаки на наши ПК и смартфоны?). Военные традиционно не слишком считаются с расходами, а формальные методы анализа кода относительно дешевы в сравнении с другими направлениями. Проблема тут скорее в поиске талантливых спецов, коих на рынке крайне мало. Но так или иначе, инвестиции в профильный софт будут возрастать -- что по военным направлениям, что из экономических соображений. Нынешние продукты будут становиться все более популярными, и простимулируют рынок далее.
Среднесрочная перспектива. Proof assistants будут активнее применяться в обучении программированию, и боты-тьюторы сынтегрируются со средами и системами разработки -- например, Coq с OCaml, а ACL2 с Lisp. Здесь очень многое зависит от ведущих университетов, и достаточно велика вероятность, что как минимум Coq/OCaml завоюет популярность в США и Европе. Так, уже заметно вкладываются в эти направления Cornell, Harvard, Princeton, UPenn, Yale, MIT... Профессор предсказывает, что тематические курсы в формате MOOC появятся уже в ближайшие пять лет.
Можно будет неплохо заработать на proof assistants, используя их в качестве экспертных систем для специализированных ниш. Например, с помощью Nuprl были созданы протоколы, устойчивые ко многим типам хакерских атак, и ряд задействованных в этом процессе концепций, вероятно, будут реализованы на уровне языков программирования.
С помощью Coq в UPenn был создан математически верифицированный Си-компилятор, Harvard использовал Coq для проверки транслирующей инфраструктуры Breeze http://www.cs.utexas.edu/users/c-breeze/, а MIT с его помощью рекурсивно верифицировал Bedrock http://plv.csail.mit.edu/bedrock/ -- библиотеку верификации для Coq.
Кроме того, proof assistants будут активно применяться в качестве помощников математиков, и тут можно ожидать новых теоретических прорывов.
Долгосрочная перспектива. Со временем люди, впервые столкнувшись с proof assistants, будут шокированы их способностями и потенциалом. Эти системы смогут решать в реальном времени сложнейшие математические теоремы, генерируя текстовое описание доказательства в Latex. Таким образом будут писаться целые книги на научную тематику, и уже сейчас ведется профильная деятельность например в проекте UPenn Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/
Как минимум в сфере формальной математики и теории вычислений это произойдет точно. Вокруг подобных подходов постепенно сформируется свое infoware, охватывающее менее специализированные области, и постепенно доберется и до средних школ. Возникнут коммьюнити, связанные через Сеть, которые будут совместными усилиями атаковать серьезнейшие математические проблемы, и научатся создавать программные системы любого объёма, правильные по построению. Проблески этого уже видны в сообществах Coq и Nuprl.
В дальней перспективе, будет проанализирована геномная информация и вообще любая информация, определяющая человека как живой вид. Мы уже будем не Homo sapiens, а Homo informatis. Это будет новый аспект нашей человечности -- мы тесно интегрируемся в информационную экосистему, а proof assistants станут неотъемлемой частью нас самих.
Далее познакомимся с инструментарием программиста, который поможет верифицировать ядро критически важной системы, исключить баги в боевом кибероружии, а в перспективе -- создать AGI , который захватит мир
[1] http://www.ruscrypto.ru/program/sections/section-06/