
11 Déc Un assistant de vérification de preuves nommé Coq
Depuis longtemps, on utilise les mathématiques pour vérifier les programmes informatiques. Il s’avère que l’informatique peut rendre la pareille aux mathématiques : pour vérifier de manière automatique une preuve mathématique, il existe des logiciels appelés assistant de preuve. La chronique Mathématiques de Nadia Lafrenière, Stéphanie Schanck et Élise Vandomme du 11 décembre 2017 nous en apprend plus sur Coq, un de ces logiciels.
No Comments