Lanzouse a versión 8.12 (a última versión menor dispoñible no momento de escribir a noticia é a 8.12.1) da ferramenta interactiva de demostración de teoremas Coq (galla).
Coq inclúe a linguaxe de programación de tipo dependente de Gallina (polo), que se basea na teoría do cálculo de construción.
O sistema Coq permítelle desenvolver demostracións de teoremas e programas verificables por ordenador xunto coa proba de conformidade coa especificación.
A nova versión mellorou significativamente a biblioteca estándar e a documentación, e tamén corrixiu unha serie de erros.
Fonte: linux.org.ru