Objavljena je verzija 8.12 (najnovija dostupna manja verzija u vrijeme pisanja vijesti je 8.12.1) interaktivnog alata za dokazivanje teorema Coq (cockerel).
Coq uključuje programski jezik zavisnog tipa Gallina (kokoš), koji je zasnovan na teoriji konstruktivnog računa.
Coq sistem vam omogućava da razvijete i kompjuterski proverljive dokaze teorema i programe zajedno sa dokazom usklađenosti sa specifikacijom.
Nova verzija je značajno poboljšala standardnu biblioteku i dokumentaciju, a ispravila je i niz grešaka.
izvor: linux.org.ru