Wie ein Lean-Beweis funktioniert – erklärt für Softwareentwickler
Anatomy of a Lean proof for software engineers
Ein Blogbeitrag zeigt anhand eines Problems aus Sipsers Lehrbuch, wie man in Lean einen formalen Beweis für die Regularität einer Sprache führt. Der Autor baut einen DFA, der die Umkehrung der Sprache erkennt, und nutzt Mathlib, um den Beweis zu vervollständigen. Der Beitrag richtet sich an Entwickler mit Kenntnissen in statisch typisierten Sprachen, binärer Arithmetik und Induktionsbeweisen.
Der schwierige Teil ist, dass wir das mit einer festen Menge an Speicher für beliebig lange Zeichenketten tun müssen.