نسخه 8.12 (آخرین نسخه مینور موجود در زمان نگارش خبر 8.12.1 است) ابزار اثبات قضیه تعاملی Coq (cockerel) منتشر شده است.
Coq شامل زبان برنامه نویسی نوع وابسته به گالینا (مرغ) است که بر اساس تئوری حساب دیفرانسیل و انتگرال است.
سیستم Coq به شما این امکان را می‌دهد که هم برنامه‌ها و هم اثبات قضیه‌های قابل تأیید با رایانه را همراه با اثبات انطباق با مشخصات توسعه دهید.
نسخه جدید کتابخانه استاندارد و اسناد را به طور قابل توجهی بهبود بخشیده است و همچنین تعدادی از خطاها را برطرف کرده است.
منبع: linux.org.ru