גרסה 8.12 שוחררה (הגרסה המינורית האחרונה הזמינה בזמן כתיבת החדשות היא 8.12.1) של הכלי להוכחת המשפט האינטראקטיבי Coq (קוקרל).
Coq כולל את שפת התכנות מסוג Gallina (עוף), המבוססת על התיאוריה של חשבון בנייה.
מערכת Coq מאפשרת לך לפתח גם הוכחות משפט הניתנות לאימות מחשב וגם תוכניות יחד עם הוכחת התאמה למפרט.
הגרסה החדשה שיפרה משמעותית את הספרייה והתיעוד הסטנדרטיים, וגם תיקנה מספר שגיאות.
מקור: linux.org.ru