13.03.2026 –, Vorträge 1 Sprache: English
Proofs about programs are great, but what happens if we let programs and proofs interact in both directions? Lean is both a programming language and an interactive theorem prover, and it provides ways of influencing the compiler using proofs. A simple example is proving that array accesses are in-bounds to guarantee that no bounds check is emitted by the compiler. Much more elaborate examples involving nontrivial properties of programs are possible, limited only by the ergonomics of the proving system.
Thanks to Lean being a competent interactive theorem prover, this is now quite practical, and we can reason about complex properties like balancing properties of binary search trees or UTF-8 decoding and encoding right as we implement them, and use proofs to make the implementations even better. In my presentation, I will walk through many examples in the Lean standard library where this interaction has enabled us to write code that is safe, fast and user-friendly all at once.
- Proofs aren't just assurance that a program works, but they can also tell a compiler how to generate better code. This idea is already present in every type system, but it can be taken much further.
- The ergonomics of interactively proving properties of programs using Lean have improved a lot in the past year(s) and are now at a point where an experienced Lean user can routinely prove nontrivial algorithmic properties of programs on the fly while programming.
- When writing a
panicin your code (in any language), you should ask yourself: am I asserting that this is a possible error condition or do I believe that this code is actually unreachable? Some languages, like Rust, make this distinction by differentiating betweenpanic!andunreachable!, but this is "just" a cosmetic/documentation difference that compiles to essentially the same code. In a language with proofs, we can convince the compiler to emit no code at all in theunreachablecase.
Markus is a tech lead at the Lean Focused Research Organization, the non-profit behind the Lean theorem prover and programming language. He leads the standard library team, helping advance Lean as a tool for developing production-ready formally verified software.