Software Unscripted Metaprogramming Your IDE in Lean 4 with Harry Goldstein
Dec 21, 2025
Harry Goldstein, a researcher in software testing and Lean 4 metaprogramming, shares his insights with Richard Feldman. They explore Lean 4's compile-time metaprogramming, particularly its ability to enhance IDEs in real-time. Harry discusses ProofWidgets, properties of totality, and the balance between trusted cores and flexible metaprogramming. They touch on security concerns with metaprogramming and the implications of property-based testing. The conversation also draws interesting parallels between Lean and Smalltalk's dynamic capabilities.
AI Snips
Chapters
Transcript
Episode notes
Compile-Time UI From The Compiler
- Lean 4's metaprogramming runs at compile time and can inject rich UI widgets into the editor.
- Harry Goldstein used this to render interactive React charts from generator output inside VS Code.
Widgets Are Editor-Agnostic Web Views
- ProofWidgets compiles React modules and injects them into VS Code webviews.
- The approach is editor-agnostic so any editor with a web view can host similar widgets.
Metaprogramming Outside The Trusted Core
- Lean limits metaprogramming to pre-core stages to preserve soundness of the trusted core.
- Arbitrary IO and nontermination are allowed during elaboration but not inside the total core.