Phiên bản 8.12 đã được phát hành (phiên bản nhỏ mới nhất có sẵn tại thời điểm viết tin là 8.12.1) của công cụ chứng minh định lý tương tác Coq (cockerel).
Coq bao gồm ngôn ngữ lập trình kiểu phụ thuộc Gallina (gà), dựa trên lý thuyết về phép tính xây dựng.
Hệ thống Coq cho phép bạn phát triển cả chương trình và bằng chứng định lý có thể kiểm chứng bằng máy tính cùng với bằng chứng về sự phù hợp với đặc tả.
Phiên bản mới đã cải thiện đáng kể thư viện và tài liệu tiêu chuẩn, đồng thời cũng sửa một số lỗi.
Nguồn: linux.org.ru