È stata rilasciata la versione 8.12 (l'ultima versione minore disponibile al momento in cui scriviamo la notizia è la 8.12.1) dello strumento interattivo per la dimostrazione di teoremi Coq (galletto).
Coq include il linguaggio di programmazione di tipo dipendente Gallina (pollo), basato sulla teoria del calcolo dei costrutti.
Il sistema Coq consente di sviluppare sia dimostrazioni di teoremi che programmi verificabili tramite computer insieme alla prova di conformità alle specifiche.
La nuova versione ha migliorato significativamente la libreria standard e la documentazione e ha anche corretto una serie di errori.
Fonte: linux.org.ru