Metaprogramming the Next Generation of Testing Tools

Abstract: Lean is an incredible platform for mathematics, but it is also an extremely capable programming language. By combining dependent types with a state-of-the-art metaprogramming system, Lean enables new approaches to writing everyday programs.

In this talk, I describe work that my colleagues and I have done over the last year that uses metaprogramming in Lean to build new tools for automated testing. I'll demonstrate how Lean's proof system can be repurposed as a system for interactive program synthesis, and I'll show off some other interactive programming interfaces that would require far more work to implement in other languages.

I hope that my talk will provide a glimpse of a new generation of testing tools and inspire others to consider the expressive power of Lean in other programming domains.

logic in computer sciencemathematical softwareprogramming languagessoftware engineering

Audience: researchers in the discipline

( video )

Lean Together 2026