Objavljena je verzija 8.12 (zadnja dostupna manja verzija u vrijeme pisanja vijesti je 8.12.1) interaktivnog alata za dokazivanje teorema Coq (pijetao).
Coq uključuje programski jezik ovisan o tipu Gallina (kokoš), koji se temelji na teoriji konstruktnog računa.
Sustav Coq omogućuje vam da razvijete i računalno provjerljive dokaze teorema i programe zajedno s dokazom usklađenosti sa specifikacijom.
Nova verzija značajno je poboljšala standardnu biblioteku i dokumentaciju, a također je ispravila brojne pogreške.
Izvor: linux.org.ru