Κυκλοφόρησε η έκδοση 8.12 (η τελευταία διαθέσιμη δευτερεύουσα έκδοση τη στιγμή της σύνταξης της είδησης είναι η 8.12.1) του διαδραστικού εργαλείου απόδειξης θεωρημάτων Coq (κοκορέτσι).
Το Coq περιλαμβάνει τη γλώσσα προγραμματισμού εξαρτώμενου τύπου Gallina (κοτόπουλο), η οποία βασίζεται στη θεωρία του λογισμού κατασκευής.
Το σύστημα Coq σάς επιτρέπει να αναπτύξετε αποδείξεις θεωρημάτων και προγράμματα που μπορούν να επαληθευτούν από υπολογιστή μαζί με απόδειξη συμμόρφωσης με τις προδιαγραφές.
Η νέα έκδοση βελτίωσε σημαντικά την τυπική βιβλιοθήκη και την τεκμηρίωση, και επίσης διόρθωσε μια σειρά σφαλμάτων.
Πηγή: linux.org.ru