La version 8.12 (la dernière version mineure disponible au moment de la rédaction de cet article – 8.12.1) de l'outil de preuve interactive de théorèmes Coq (coq) est sortie.
Coq comprend un langage de programmation à types dépendants appelé Gallina (poule), basé sur la théorie des constructions.
Le système Coq permet de développer à la fois des preuves de théorèmes vérifiables sur ordinateur et des programmes accompagnés de preuves de conformité à la spécification.
Dans cette nouvelle version, la bibliothèque standard et la documentation ont été considérablement améliorées, et plusieurs bogues ont été corrigés.
Source : linux.org.ru
