A fost lansată versiunea 8.12 (cea mai recentă versiune minoră disponibilă la momentul redactării știrii – 8.12.1) a instrumentului de dovadă interactivă a teoremelor Coq (cocoșul).
Coq include un limbaj de programare cu tipuri dependente Gallina (găina), bazat pe teoria calculului construcțiilor.
Sistemul Coq permite dezvoltarea atât a dovezilor teoremelor verificate computațional, cât și a programelor împreună cu dovezi de conformitate cu specificația.
În noua versiune, biblioteca standard și documentația au fost semnificativ îmbunătățite, precum și corectate o serie de erori.
Sursa: linux.org.ru
