Foi lançada a versão 8.12 (a última versão menor disponível no momento da redação da notícia – 8.12.1) da ferramenta de prova interativa de teoremas Coq (galo).
Coq inclui uma linguagem de programação com tipos dependentes Gallina (galinha), baseada na teoria do cálculo de construções.
O sistema Coq permite desenvolver tanto provas teóricas verificáveis por computador quanto programas junto com a prova de conformidade com a especificação.
Na nova versão, a biblioteca padrão e a documentação foram significativamente aprimoradas, além de uma série de erros terem sido corrigidos.
Fonte: linux.org.ru
