Излезе версия 8.12 (последната налична минорна версия към момента на написване на новината – 8.12.1) на инструмента за интерактивно доказателство на теореми Coq (петльо).
Coq включва език за програмиране с зависими типове Gallina (петел), основан на теорията на конструкции.
Системата Coq позволява разработването както на компютърно проверими доказателства на теореми, така и на програми с доказателство за съответствие на спецификацията.
В новата версия беше значително подобрена стандартната библиотека и документацията, както и бяха отстранени редица грешки.
Източник: linux.org.ru
