Dans le numéro de juin 2026 de Communications of the ACM, Christine Paulin-Mohring revient sur quarante ans de développement de Rocq (anciennement Coq), l'un des assistants de preuve les plus utilisés pour vérifier formellement la correction de programmes et de démonstrations mathématiques. Elle y évoque ses contributions fondatrices, son travail sur la bibliothèque ALEA pour les programmes probabilistes, et l'évolution des usages de Rocq, aujourd'hui mobilisé aussi bien pour la vérification de compilateurs que pour l'enseignement des mathématiques.
Lire l'entretien complet sur Communications of the ACM.