Coq 8.12

Versjon 8.12 (den siste tilgjengelige minorversjonen på tidspunktet for skrivingen av nyheten – 8.12.1) av verktøyet for interaktiv bevisføring av teoremer Coq (hane) er lansert.

Coq inkluderer et programmeringsspråk med avhengige typer, Gallina (høne), basert på teorien om konstruksjonsberegning.

Coq-systemet lar deg utvikle både dataverifiserbare bevis for teoremer og programmer sammen med bevis for samsvar med spesifikasjonen.

Den nye versjonen har gjennomgått betydelige forbedringer av standardbiblioteket og dokumentasjonen, samt at en rekke feil er rettet.

Kilde: linux.org.ru