Wydano wersję 8.12 (ostatnia dostępna wersja minor na moment pisania wiadomości – 8.12.1) narzędzia interaktywnego dowodzenia twierdzeń Coq (kogut).
Coq zawiera język programowania z zależnymi typami Gallina (kurczak), oparty na teorii konstrukcji obliczeniowych.
System Coq pozwala na opracowywanie zarówno formalnych dowodów twierdzeń, jak i programów wraz z dowodami spełnienia specyfikacji.
W nowej wersji znacznie poprawiono standardową bibliotekę i dokumentację, a także naprawiono szereg błędów.
Źródło: linux.org.ru
