Produire des logiciels sans bug et qui font ce qu’ils sont supposés faire relève parfois du miracle. En plus des tests, des outils formels issus de la logique et des mathématiques sont utilisés pour garantir leur fiabilité. Spécialiste de la sémantique des langages, Xavier Leroy nous livre ses réflexions sur la programmation.