Version 8.12 er blevet frigivet (den seneste tilgængelige mindre version i skrivende stund er 8.12.1) af det interaktive teorembevisværktøj Coq (cockerel).
Coq inkluderer det Gallina (kylling) afhængige type programmeringssprog, som er baseret på teorien om konstruktionsregning.
Coq-systemet giver dig mulighed for at udvikle både computerverificerbare teorembeviser og programmer sammen med bevis for overensstemmelse med specifikationen.
Den nye version har forbedret standardbiblioteket og dokumentationen markant og også rettet en række fejl.
Kilde: linux.org.ru