Versiunea 8.12 a fost lansată (cea mai recentă versiune minoră disponibilă la momentul scrierii știrii este 8.12.1) a instrumentului interactiv de demonstrare a teoremei Coq (cocoș).
Coq include limbajul de programare de tip dependent Gallina (pui), care se bazează pe teoria calculului de construcție.
Sistemul Coq vă permite să dezvoltați atât dovezi de teoreme, cât și programe verificabile de calculator, împreună cu dovezi de conformitate cu specificația.
Noua versiune a îmbunătățit semnificativ biblioteca și documentația standard și, de asemenea, a remediat o serie de erori.
Sursa: linux.org.ru