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