S'ha llançat la versió 8.12 (l'última versió menor disponible en el moment d'escriure la notícia és la 8.12.1) de l'eina interactiva de demostració de teoremes Coq (gall).
Coq inclou el llenguatge de programació de tipus dependent de Gallina (pollastre), que es basa en la teoria del càlcul constructiu.
El sistema Coq us permet desenvolupar tant demostracions de teoremes com programes verificables per ordinador juntament amb proves de conformitat amb l'especificació.
La nova versió ha millorat significativament la biblioteca i la documentació estàndard, i també ha corregit una sèrie d'errors.
Font: linux.org.ru