Вийшла версія 8.12 (остання доступна мінорна версія на момент написання новини – 8.12.1) інструменту інтерактивного доказу теорем Coq (півник).
Coq включає мову програмування із залежними типами Gallina (курка), що спирається на теорію обчислення конструкцій.
Система Coq дозволяє розробляти як комп'ютерно-верифіковані докази теорем, так і програми разом із доказом відповідності специфікації.
У новій версії було значно доопрацьовано стандартну бібліотеку та документацію, а також виправлено низку помилок.
Джерело: linux.org.ru