Se ha lanzado la versión 8.12 (la última versión menor disponible en el momento de escribir esta noticia es 8.12.1) de la herramienta de prueba interactiva de teoremas Coq (gallo).
Coq incluye un lenguaje de programación con tipos dependientes Gallina (gallina), que se basa en la teoría de los cálculos constructivos.
El sistema Coq permite desarrollar tanto pruebas de teoremas verificables por ordenador como programas junto con pruebas de correspondencia con la especificación.
En la nueva versión, se ha mejorado significativamente la biblioteca estándar y la documentación, y se han corregido varios errores.
Fuente: linux.org.ru
