Izkazala se je različica 8.12 (zadnja dostopna manjšinska različica v času pisanja novice – 8.12.1) orodja za interaktivno dokazovanje teorem Coq (petelin).
Coq vključuje jezik programiranja z odvisnimi tipi Gallina (piščanec), ki temelji na teoriji konstruktivnega računanja.
Sistem Coq omogoča razvoj tako računalniško preverjenih dokazov teorem kot tudi programov skupaj z dokazom skladnosti specifikacije.
V novi različici je bila znatno izboljšana standardna knjižnica in dokumentacija, prav tako so bili odpravljeni nekateri hrošči.
Izvor: linux.org.ru
