Versioni 8.12 ka dalĂ« (versioni mĂ« i fundit minor nĂ« momentin e shkrimit tĂ« lajmit â 8.12.1) i mjetit tĂ« provave interaktive tĂ« teoremave Coq (kukuvajkĂ«).
Coq përfshin një gjuhë programimi me tipe të varura Gallina (pjepër), e cila bazohet në teorinë e llogaritjeve konstruktive.
Sistemi Coq lejon zhvillimin e provave të teoremave që mund të verifikohen nga kompjuteri, si dhe programeve së bashku me provën e përputhshmërisë me specifikimin.
Në versionin e ri, biblioteka standarde dhe dokumentacioni janë përmirësuar ndjeshëm, dhe janë rregulluar disa gabime.
Burimi: linux.org.ru
