Erlang Extraction Language for Coq Свершилось, то что завещал великий Лямбдагарбха. Некто @tcarstens зарелизил на гитхабе 2 дня назад рабочий прототип экстрактора Core Erlang для Coq: https://github.com/tcarstens/verlang. В Сoq экстракция программ происходит в MiniML, который уже потом транслируется в Core Erlang. Поэтому есть ньюансы: - Erlang не поддерживается модули в модулях (генерируется имя) - В эрланге нет каррирования (это пока не решено) - В МиниМЛ нет аналога receive (в Coq воодится доп аксиома) В примере доказательство hashtree которое экстрактится в эрланг. Другие Экстракторы мейнстрима для Coq: Ruby -- https://github.com/mzp/coq-ruby Clojure -- http://patch-tag.com/r/leque/coq-clojure-ext/home JavaScript -- https://bitbucket.org/yoshihiro503/coq2javascript SML/NJ -- https://bitbucket.org/yoshihiro503/coq2sml Scala -- https://bitbucket.org/yoshihiro503/coqincoq_scala Напомнить для неискушенных читателей что экстракторы Scheme, Haskell и OCaml являются дефаултными в Сoq. И совершенно няшное комюнити http://www.proofcafe.org/ P.S. http://sole.dimi.uniud.it/~marino.miculan/wordpress/downloads/erlang-coq-synthesizer