Metaprogramming Your IDE in Lean 4 with Harry Goldstein

Metaprogramming Your IDE in Lean 4 with Harry Goldstein

From Software Unscripted by Richard Feldman

December 21, 2025 · 41 min

About this episode

Harry Goldstein discusses Lean 4's metaprogramming capabilities and their application in IDEs with Richard Feldman.

Harry Goldstein talks with Richard Feldman about the Lean 4 programming language's compile-time metaprogramming capabilities, including how they can be used to control elements of your IDE in realtime. They also discuss other topics like property-based testing, theorem proving, and Smalltalk. You can get ad-free episodes (including video) by supporting Software Unscripted on Patreon! https://www.patreon.com/SoftwareUnscripted The Best New Programming Language is a Proof Assistant by Harry Goldstein - https://youtu.be/c5LOYzZx-0c?si=UnTfkczIhdoF7Qkx The Lean Programming Language - https://lean-lang.org Simon Peyton-Jones: Escape from the ivory tower: the Haskell journey - https://youtu.be/re96UgMk6GQ?si=8xqpAS8VTQaqgbzg "Shen: A Sufficiently Advanced Lisp" by Aditya Siram - https://youtu.be/lMcRBdSdO_U?si=VOwJNeLAvnIRUm_n Hypothesis Property-Based Testing library for Python - https://hypothesis.works/ Hosted on Acast. See acast.com/privacy for more information.

People in this episode

Host: Richard Feldman

Guest: Harry Goldstein

Topics covered

  • metaprogramming
  • Lean 4
  • IDE
  • property-based testing
  • theorem proving
  • Smalltalk

Keywords

  • Lean 4
  • metaprogramming
  • IDE
  • property-based testing
  • theorem proving
  • Smalltalk

Mentioned in this episode

Organizations: Software Unscripted, Hypothesis Property-Based Testing

Books & works: The Best New Programming Language is a Proof Assistant, The Lean Programming Language, Escape from the ivory tower: the Haskell journey, Shen: A Sufficiently Advanced Lisp

More episodes of Software Unscripted

Explore listener stats, chart rankings, contacts and more on the Software Unscripted podcast page.