Version 8.12 har släppts (den senaste tillgängliga mindre versionen när nyheten skrivs är 8.12.1) av det interaktiva teorembevisverktyget Coq (cockerel).
Coq inkluderar det Gallina (kyckling) beroende typ av programmeringsspråk, som är baserat på teorin om konstruktionskalkyl.
Coq-systemet låter dig utveckla både datorverifierbara teorembevis och program tillsammans med bevis på överensstämmelse med specifikationen.
Den nya versionen har avsevärt förbättrat standardbiblioteket och dokumentationen, och även åtgärdat ett antal fel.
Källa: linux.org.ru