Episode
Metaprogramming Your IDE in Lean 4 with Harry Goldstein
- Podcast
- Software Unscripted
- Published
- Dec 21, 2025
- Duration seconds
- 2478
- Processing state
not_requested- Canonical source
- https://shows.acast.com/software-unscripted/episodes/metaprogramming-your-ide-in-lean-4-with-harry-goldstein
Actions
POST https://stenobird.com/v1/public/podcasts/software-unscripted-5320480/episodes/metaprogramming-your-ide-in-lean-4-with-harry-goldstein/transcription-requests
Idempotently request low-priority transcript generation for this episode.GET https://stenobird.com/podcast/software-unscripted-5320480/metaprogramming-your-ide-in-lean-4-with-harry-goldstein.md
Read the agent-friendly Markdown representation of this episode resource.
Summary
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.