Die Version 8.12 (die letzte verfügbare Minor-Version zum Zeitpunkt der Erstellung dieser Nachricht – 8.12.1) des interaktiven Beweiswerkzeugs Coq (Hahn) ist erschienen.
Coq enthält eine Programmiersprache mit abhängigen Typen Gallina (Huhn), die auf der Theorie des Konstruktionskalküls basiert.
Das Coq-System ermöglicht die Entwicklung sowohl computergestützter, überprüfbarer Beweise als auch Programme zusammen mit einem Nachweis über die Übereinstimmung mit den Spezifikationen.
In der neuen Version wurde die Standardbibliothek und die Dokumentation erheblich überarbeitet, und es wurden mehrere Fehler behoben.
Quelle: linux.org.ru
