Ir izlaista interaktīvā teorēmu pierādīšanas rīka Coq (gailītis) versija 8.12 (jaunākā pieejamā neliela versija ziņu rakstīšanas laikā ir 8.12.1).
Coq ietver Gallina (vistas) atkarīgā tipa programmēšanas valodu, kas ir balstīta uz konstrukcijas aprēķinu teoriju.
Coq sistēma ļauj izstrādāt gan datorā pārbaudāmus teorēmu pierādījumus, gan programmas, kā arī atbilstības apliecinājumu specifikācijai.
Jaunā versija ir būtiski uzlabojusi standarta bibliotēku un dokumentāciju, kā arī izlabojusi vairākas kļūdas.
Avots: linux.org.ru