Bola vydaná verzia 8.12 (posledná dostupná vedľajšia verzia v čase písania správy je 8.12.1) interaktívneho nástroja na dokazovanie teorémov Coq (kohútik).
Coq obsahuje programovací jazyk závislý od typu Gallina (kura), ktorý je založený na teórii konštrukčného počtu.
Systém Coq vám umožňuje vyvíjať počítačom overiteľné dôkazy teorémov a programy spolu s dôkazom zhody so špecifikáciou.
Nová verzia výrazne zlepšila štandardnú knižnicu a dokumentáciu a opravila aj množstvo chýb.
Zdroj: linux.org.ru