Isabelle est un assistant de preuve.

Je l'utilise dans mon cours Sémantique des langages en mention Sciences du logiciel.

Preuve de la correction du programme de l'épisode "Program Correctness" de Computerphile

L'épisode "Program Correctness" du 27 novembre 2020 sur la chaîne Youtube Computerphile présente un petit programme compilant des expressions très simples vers une machine d'exécution. Voici la preuve de sa correction en Isabelle.

Équivalence des définitions du PGCD sur les entiers

Pour prouver la correction de l'algorithme d'Euclide (par soustractions successives), on utilise la définition suivante du PGCD :

Le pgcd de {$a$} et {$b$} est un diviseur commun de {$a$} et {$b$} tel que tout autre diviseur commun de {$a$} et {$b$} le divise.

Pour les entiers, on utilise habituellement une définition du PGCD fondée sur l'ordre :

Le pgcd de {$a$} et {$b$} est un diviseur commun de {$a$} et {$b$} tel que tout autre diviseur commun de {$a$} et {$b$} lui est inférieur.

L'équivalence de ces deux définitions peut être démontrée avec Isabelle.

Preuves de propriétés mathématiques

Isabelle se prête également bien à la preuve de propriétés mathématiques dans le cours d'algorithmique de première année : preuves du cours d'algorithmes en 1A.