È stata rilasciata la versione 8.12 (l'ultima versione minore disponibile al momento della scrittura della notizia – 8.12.1) dello strumento di dimostrazione interattiva dei teoremi Coq (il gallo).
Coq include un linguaggio di programmazione con tipi dipendenti Gallina (la gallina), basato sulla teoria dei calcoli induttivi.
Il sistema Coq consente di sviluppare sia prove di teoremi verificabili da computer che programmi, insieme alla dimostrazione di conformità alle specifiche.
Nella nuova versione sono stati notevolmente migliorati la libreria standard e la documentazione, ed è stato corretto un numero di errori.
Fonte: linux.org.ru
