Versi 8.12 (versi minor terbaru yang tersedia saat penulisan ini adalah 8.12.1) dari alat pembuktian teorema interaktif Coq (rooster) telah dirilis.
Coq mencakup bahasa pemrograman Gallina (Chicken) dengan tipe dependen, berdasarkan teori kalkulus konstruk.
Sistem Coq memungkinkan pengembangan bukti teorema yang dapat diverifikasi komputer dan program beserta bukti kesesuaian dengan spesifikasi.
Versi baru ini menyertakan perbaikan signifikan pada pustaka dan dokumentasi standar, serta sejumlah perbaikan bug.
Sumber: linux.org.ru
