Тихо и незаметно вышла новая версия системы интерактивного доказательства теорем Coq (Петух).Система Coq предоставляет язык Gallina (Курица) — функциональный язык с зависимыми типами, основанный на исчислении индуктивных конструкций. Особенностью данной системы является наличие особого подъязыка тактик доказательства (в отличии от, например, Агды, в которой пользователь конструирует элемент типа, являющийся доказательством, в явном виде с использованием интерактивного интерфейса, основанного на Emacs).Coq используется как собственно в математике, так и для так называемого сертифицированного программирования — написания программ вместе с доказательством их корректности.Основные новшества в версии 8.5: асинхронное редактирование документов в CoqIDE, позволяющее работать с текущим доказательством, в то время как Coq проверяет другие доказательства в фоне; полиморфизм относительно универсумов, позволяющий использовать одни и те же определения для универсумов разного уровня; примитивные проекции, улучшающие временную и пространственную эффективность для записей и добавляющие для них эта-конверсию; новый движок тактик; новая процедура редукции native_compute, позволяющая вычислять термы, используя нативный компилятор OCaml'а; новый быстрый режим компиляции, пропускающий проверку доказательств; новая опция -type-in-type, позволяющая объединять иерархию типов в один универсум (делает логику несогласованной, но упрощает эксперименты); заметное улучшение эффективности в целом.
Ссылка: http://www.linux.org.ru/news/opensource/12300606