Lean 4.22 : Une nouvelle infrastructure de vérification pour les programmes impératifs
Lean 4.22 introduit une nouvelle fonctionnalité passionnante : une nouvelle infrastructure de vérification pour prouver les propriétés des programmes impératifs. L’article utilise un exemple simple — déterminer si une liste contient deux entiers dont la somme est égale à zéro — pour démontrer l’utilisation de cette fonctionnalité et la comparer à des outils similaires tels que Dafny et Verus. Le nouveau framework, Std.Do, utilise des triplets de Hoare et combine les tactiques `mvcgen` et `grind` pour simplifier considérablement le processus de vérification des programmes impératifs, même ceux comportant un flux de contrôle complexe comme des boucles et des retours anticipés. Contrairement aux systèmes automatisés qui reposent sur des solveurs SMT externes, l’approche de preuve interactive de Lean offre une meilleure fiabilité, une débogage plus facile et une meilleure maintenabilité, ce qui en fait un choix convaincant pour les tâches de vérification de programmes en environnement réel.
