Écrire des programmes prouvés corrects avec Coq (fr)

Dans le présent article, nous montrerons sur un exemple à quoi ressemble l’écriture de programmes prouvés corrects avec l’assistant de preuve Coq. Il s’agit d’un logiciel permettant de faire des démonstrations mathématiques, qui a la particularité d’intégrer aussi un langage de programmation et qui permet ainsi de mêler programmation et preuves mathématiques. Il n’est pas nécessaire de connaître Coq pour suivre cet article puisque les explications permettent de suivre l’essentiel du propos.