Versi 8.12 telah dirilis (versi minor terbaru yang tersedia pada saat berita ini ditulis adalah 8.12.1) dari alat pembuktian teorema interaktif Coq (cockerel).
Coq termasuk bahasa pemrograman tipe dependen Gallina (ayam), yang didasarkan pada teori kalkulus konstruk.
Sistem Coq memungkinkan Anda mengembangkan bukti dan program teorema yang dapat diverifikasi komputer serta bukti kesesuaian dengan spesifikasi.
Versi baru ini telah meningkatkan pustaka dan dokumentasi standar secara signifikan, dan juga memperbaiki sejumlah kesalahan.
Sumber: linux.org.ru