Lean 4.22: Eine neue Verifikationsinfrastruktur für imperative Programme

Lean 4.22 führt ein aufregendes neues Feature ein: eine neue Verifikationsinfrastruktur zum Beweisen von Eigenschaften imperativer Programme. Der Beitrag verwendet ein einfaches Beispiel – die Bestimmung, ob eine Liste zwei ganze Zahlen enthält, die sich zu Null summieren – um die Verwendung des Features zu demonstrieren und vergleicht es mit ähnlichen Tools wie Dafny und Verus. Das neue Framework, Std.Do, verwendet Hoare-Tripel und kombiniert die Taktiken `mvcgen` und `grind`, um den Verifikationsprozess für imperative Programme erheblich zu vereinfachen, sogar für solche mit komplexem Kontrollfluss wie Schleifen und vorzeitigen Rückgaben. Im Gegensatz zu automatisierten Systemen, die auf externe SMT-Solver angewiesen sind, bietet der interaktive Beweisansatz von Lean eine höhere Zuverlässigkeit, einfacheres Debugging und bessere Wartbarkeit, was es zu einer überzeugenden Wahl für reale Programmierverifikationsaufgaben macht.