Vyšla verzia 8.12 (posledná dostupná menšia verzia v čase písania novinky – 8.12.1) nástroja na interaktívne dokazovanie teórií Coq (kohút).
Coq obsahuje programovací jazyk so závislými typmi Gallina (kurča), ktorý sa zakladá na teórii konštrukčných výpočtov.
Systém Coq umožňuje vyvíjať ako počítačom overiteľné dôkazy teórií, tak aj programy spolu s dôkazom zhody so špecifikáciou.
V novej verzii bola značně vylepšená štandardná knižnica a dokumentácia, ako aj opravených niekoľko chýb.
Zdroj: linux.org.ru
