D'Versioun 8.12 gouf verëffentlecht (déi lescht verfügbar kleng Versioun zum Zäitpunkt vum Schreiwen vun der Neiegkeet ass 8.12.1) vum interaktiven Theorem Beweisinstrument Coq (Cockerel).
Coq enthält d'Gallina (Huhn) ofhängeg Typ Programméierungssprooch, déi op der Theorie vum Konstruktkalkulus baséiert.
De Coq System erlaabt Iech souwuel Computer-verifizéierbar Theorem Beweiser a Programmer z'entwéckelen zesumme mat Beweis vu Konformitéit mat der Spezifizéierung.
Déi nei Versioun huet d'Standardbibliothéik an d'Dokumentatioun wesentlech verbessert, an och eng Rei vu Feeler fixéiert.
Source: linux.org.ru