เวอร์ชัน 8.12 ได้รับการเผยแพร่แล้ว (เวอร์ชันรองล่าสุดที่มีอยู่ ณ เวลาที่เขียนข่าวคือ 8.12.1) ของเครื่องมือพิสูจน์ทฤษฎีบทเชิงโต้ตอบ Coq (กระทง)
Coq รวมภาษาการเขียนโปรแกรมประเภท Gallina (ไก่) ซึ่งอิงตามทฤษฎีแคลคูลัสโครงสร้าง
ระบบ Coq ช่วยให้คุณสามารถพัฒนาทั้งการพิสูจน์ทฤษฎีบทและโปรแกรมที่ตรวจสอบได้ด้วยคอมพิวเตอร์ พร้อมกับการพิสูจน์ความสอดคล้องกับข้อกำหนด
เวอร์ชันใหม่ได้ปรับปรุงไลบรารีมาตรฐานและเอกสารประกอบอย่างมาก และยังแก้ไขข้อผิดพลาดจำนวนหนึ่งด้วย
ที่มา: linux.org.ru