Izšla je različica 8.12 (zadnja razpoložljiva manjša različica v času pisanja novice je 8.12.1) interaktivnega orodja za dokazovanje izrekov Coq (petelin).
Coq vključuje programski jezik, odvisen od vrste Gallina (piščanec), ki temelji na teoriji konstruktnega računa.
Sistem Coq vam omogoča, da razvijete računalniško preverljive dokaze izrekov in programe skupaj z dokazom o skladnosti s specifikacijo.
Nova različica je znatno izboljšala standardno knjižnico in dokumentacijo ter odpravila številne napake.
Vir: linux.org.ru