[spoiler]
предыдущий пост по теме http://www.pcweek.ru/idea/blog/idea/6489.php
Самым первым инструментом в контексте автоматического синтеза программ, правильных по построению, стал NuPRL http://www.nuprl.org/ , созданный в 1979-м в Cornell University, через пять лет завоевавший признание профильной математической тусовки. Его логика базируется на Computational Type Theory, а развитие продолжается и по сей день, поэтому в систему заложен мощный потенциал.
Российские математики этим сервисом активно пользуются. Вот, например, решена проблема, стоявшая еще с 1930 г. -- формализована семантика Брауэра-Гейтинга-Колмогорова для интуиционистской логики. http://lpcs.math.msu.su/rus/lpcsrep.htm
Наверное, самый популярный на сегодня продукт -- это Coq http://coq.inria.fr/ , интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования Gallina с зависимыми типами (которые могут быть индексированы значениями других типов). Его разработка поддерживалась французским правительством через институт INRIA, который создал объектно-ориентированный язык функционального программирования OCaml (http://caml.inria.fr/ интерпретатор, компилятор в байткод и оптимизирующий компилятор в машинный код), ориентированный как раз на обеспечение безопасности и надежности кода.
Coq сегодня широко преподается и активно используется как помощник программистам для проверки правильности кода с использованием концепции "доказательства как программы" ("извлечение"-генерация кода из формального процесса доказательства достижимости цели).
Вот еще основные системы must have.
По направлению синтеза программ:
Agda http://wiki.portal.chalmers.se/agda/ -- чистый функциональный язык программирования с зависимыми типами, основанный на интуиционистской теории типов Мартин-Лёфа, а также система автоматического доказательства. Похож на Haskell, на котором и написан;
Minlog http://www.mathematik.uni-muenchen.de/~logik/minlog/ -- интерактивная система доказательств, созданная в University of Munich, реализующая парадигму proofs-as-programs;
MetaPRL http://metaprl.org/ -- лямбда-исчисления с зависимыми типами для кодирования логических исчислений. Состоит из двух частей -- логический фреймворк, обеспечивающий семантическую связь с языками программирования, и исполнительная система из интеллектуального решателя и механизма интерактивных доказательств. В целом -- мощная среда логического программирования, спонсируемая военным агентством передовых исследований США DARPA.
По направлению верификации программ:
ACL2 http://www.cs.utexas.edu/users/moore/acl2/ (A Computational Logic for Applicative Common Lisp) -- язык программирования для моделирования работы компьютера и система доказательств. Его используют AMD, Centaur Techology, IBM, Intel, Oracle и Rockwell Collins;
HOL (Higher Order Logic) -- семейство интеллектуальных решателей на базе логики высших порядков. Последняя версия -- http://hol.sourceforge.net/
HOL Light https://code.google.com/p/hol-light/ -- an interactive LCF-style theorem prover for classical higher order logic;
Isabelle-HOL -- http://isabelle.in.tum.de/ преемник идей HOL. Увлекательное обсуждение тематики верификации в комментах: http://habrahabr.ru/post/148709/
"Как говаривал Михаил Романович Шура-Бура, переход от неформального к формальному существенно неформален" (с)
PVS http://pvs.csl.sri.com/ -- развитая система верификации, специализированный язык и модуль доказательств.
Каждая из этих систем по своему интересна и уникальна, все они уже внесли существенный вклад в программную инженерию, и при этом остаются весьма амбициозными.
