Ang Bersyon 8.12 gipagawas na (ang pinakabag-o nga magamit nga menor de edad nga bersyon sa panahon sa pagsulat sa balita mao ang 8.12.1) sa interactive theorem nga nagpamatuod nga himan nga Coq (cockerel).
Ang Coq naglakip sa Gallina (chicken) dependent type programming language, nga gibase sa teorya sa construct calculus.
Ang sistema sa Coq nagtugot kanimo sa pag-ugmad sa duha ka computer-verifiable theorem nga mga pruweba ug mga programa uban sa pruweba sa pagpahiuyon sa espesipikasyon.
Ang bag-ong bersyon nakapauswag pag-ayo sa sumbanan nga librarya ug dokumentasyon, ug nag-ayo usab sa daghang mga sayup.
Source: linux.org.ru