Byla vydána verze 8.12 (poslední dostupná menší verze v době psaní této zprávy – 8.12.1) interaktivního nástroje pro dokazování teorémů Coq (kohout).
Coq obsahuje programovací jazyk se závislými typy Gallina (slepička), který se opírá o teorii konstrukčního kalkulu.
Systém Coq umožňuje vyvíjet jak počítačem ověřitelné důkazy teorémů, tak programy společně s důkazem shody se specifikací.
V nové verzi byla významně přepracována standardní knihovna a dokumentace, a byl opraven řada chyb.
Zdroj: linux.org.ru
