Version 8.12 wurde veröffentlicht (die letzte verfügbare Nebenversion zum Zeitpunkt des Schreibens der Nachricht ist 8.12.1) des interaktiven Theorembeweistools Coq (Hahn).
Coq beinhaltet die abhängige Programmiersprache Gallina (Huhn), die auf der Theorie der Konstruktrechnung basiert.
Mit dem Coq-System können Sie sowohl computerüberprüfbare Theorembeweise als auch Programme sowie den Nachweis der Konformität mit der Spezifikation entwickeln.
Die neue Version hat die Standardbibliothek und Dokumentation deutlich verbessert und zudem eine Reihe von Fehlern behoben.
Source: linux.org.ru