A versione 8.12 hè stata liberata (l'ultima versione minore dispunibule à u mumentu di a scrittura di a nutizia hè 8.12.1) di l'uttellu interattivu di prova di teorema Coq (cockerel).
Coq include a lingua di prugrammazione dipendente di Gallina (gallina), chì hè basatu annantu à a teoria di u calculu di custruzzione.
U sistema Coq vi permette di sviluppà sia prove di teorema verificabile per computer è prugrammi cù prova di cunfurmità cù a specificazione.
A nova versione hà migliuratu significativamente a libreria standard è a documentazione, è hà ancu correttu una quantità di errori.
Source: linux.org.ru