Выйшла версія 8.12 (апошняя даступная мінорная версія на момант напісання навіны – 8.12.1) інструмента інтэрактыўнага доказу тэарэм Coq (пеўнік).
Coq уключае ў сябе мову праграмавання з залежнымі тыпамі Gallina (курыца), які абапіраецца на тэорыю вылічэння канструкцый.
Сістэма Coq дазваляе распрацоўваць як кампутарна-верыфікаваныя доказы тэарэм, так і праграмы разам з доказам адпаведнасці спецыфікацыі.
У новай версіі была значна дапрацавана стандартная бібліятэка і дакументацыя, а таксама выпраўлены шэраг памылак.
Крыніца: linux.org.ru