È 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 (gallo).
Coq include un linguaggio di programmazione con tipi dipendenti Gallina (gallina), basato sulla teoria dei calcoli delle costruzioni.
Il sistema Coq consente di sviluppare sia prove di teoremi verificabili da computer sia programmi insieme alla prova di conformità alle specifiche.
Nella nuova versione è stata notevolmente migliorata la libreria standard e la documentazione, oltre a essere stati corretti diversi errori.
Fonte: linux.org.ru
