Buvo išleista interaktyvaus teoremų įrodinėjimo įrankio Coq (cockerel) versija 8.12 (naujausia prieinama nedidelė versija naujienų rašymo metu yra 8.12.1).
Coq apima Gallina (vištienos) priklausomo tipo programavimo kalbą, kuri remiasi konstruktyvaus skaičiavimo teorija.
Coq sistema leidžia kurti ir kompiuteriu patikrinamus teoremų įrodymus, ir programas bei atitikties specifikacijai įrodymus.
Naujoji versija žymiai patobulino standartinę biblioteką ir dokumentaciją, taip pat ištaisė daugybę klaidų.
Šaltinis: linux.org.ru