Megjelent a Coq (kakas) interaktív tételbizonyító eszköz 8.12-es verziója (a legfrissebb elérhető kisebb verzió a hír írásakor a 8.12.1).
A Coq tartalmazza a Gallina (csirke) függő típusú programozási nyelvet, amely a konstruktív kalkulus elméletén alapul.
A Coq rendszer lehetővé teszi számítógéppel ellenőrizhető tételbizonyítások és programok fejlesztését, valamint a specifikációnak való megfelelőség igazolását.
Az új verzió jelentősen javította a szabványos könyvtárat és a dokumentációt, és számos hibát is javított.
Forrás: linux.org.ru