Została wydana wersja 8.12 (najnowsza dostępna wersja dodatkowa w chwili pisania tego newsa to 8.12.1) interaktywnego narzędzia do dowodzenia twierdzeń Coq (kogucik).
Coq obejmuje język programowania typu zależnego Gallina (kurczak), który opiera się na teorii rachunku konstruktów.
System Coq umożliwia opracowywanie zarówno weryfikowalnych komputerowo dowodów twierdzeń, jak i programów wraz z dowodem zgodności ze specyfikacją.
Nowa wersja znacznie poprawiła standardową bibliotekę i dokumentację, a także naprawiła szereg błędów.
Źródło: linux.org.ru