Versi 8.12 telah dikeluarkan (versi kecil terkini yang tersedia pada masa penulisan berita ialah 8.12.1) alat pembuktian teorem interaktif Coq (ayam sabung).
Coq termasuk bahasa pengaturcaraan jenis bergantung kepada Gallina (ayam), yang berdasarkan teori kalkulus konstruk.
Sistem Coq membolehkan anda membangunkan kedua-dua bukti teorem dan program yang boleh disahkan komputer bersama-sama dengan bukti pematuhan kepada spesifikasi.
Versi baharu telah meningkatkan pustaka dan dokumentasi standard dengan ketara, dan juga membetulkan beberapa ralat.
Sumber: linux.org.ru