A versão 8.12 foi lançada (a versão secundária mais recente disponível no momento em que a notícia foi escrita é 8.12.1) da ferramenta interativa de prova de teoremas Coq (galo).
Coq inclui a linguagem de programação do tipo dependente Gallina (galinha), que é baseada na teoria do cálculo de construção.
O sistema Coq permite desenvolver provas e programas de teoremas verificáveis por computador, juntamente com provas de conformidade com a especificação.
A nova versão melhorou significativamente a biblioteca e a documentação padrão e também corrigiu vários erros.
Fonte: linux.org.ru