Versjon 8.12 har blitt utgitt (den siste tilgjengelige mindre versjonen på tidspunktet for skriving av nyhetene er 8.12.1) av det interaktive teorembevisverktøyet Coq (cockerel).
Coq inkluderer det Gallina (kylling) avhengige programmeringsspråket, som er basert på teorien om konstruksjonskalkyle.
Coq-systemet lar deg utvikle både dataverifiserbare teorembevis og programmer sammen med bevis på samsvar med spesifikasjonen.
Den nye versjonen har forbedret standardbiblioteket og dokumentasjonen betydelig, og også fikset en rekke feil.
Kilde: linux.org.ru