La version 8.12 a été publiée (la dernière version mineure disponible au moment de la rédaction de l'article est la 8.12.1) de l'outil interactif de preuve de théorèmes Coq (coq).
Coq inclut le langage de programmation de type dépendant Gallina (poulet), basé sur la théorie du calcul des constructions.
Le système Coq vous permet de développer à la fois des preuves et des programmes de théorèmes vérifiables par ordinateur ainsi que des preuves de conformité à la spécification.
La nouvelle version a considérablement amélioré la bibliothèque et la documentation standard, et a également corrigé un certain nombre d'erreurs.
Source: linux.org.ru