# Metaprogramming Your IDE in Lean 4 with Harry Goldstein

Page: https://stenobird.com/podcast/software-unscripted-5320480/metaprogramming-your-ide-in-lean-4-with-harry-goldstein
Text version: https://stenobird.com/podcast/software-unscripted-5320480/metaprogramming-your-ide-in-lean-4-with-harry-goldstein.md
Podcast: [Software Unscripted](https://stenobird.com/podcast/software-unscripted-5320480)
Published: 2025-12-21T20:18:10+00:00
Episode link: https://shows.acast.com/software-unscripted/episodes/metaprogramming-your-ide-in-lean-4-with-harry-goldstein
Audio file: https://sphinx.acast.com/p/open/s/664fde3eda02bb0012bad909/e/69485602f7567117397e5223/media.mp3
Processing state: not_requested
JSON: https://stenobird.com/v1/public/podcasts/software-unscripted-5320480/episodes/metaprogramming-your-ide-in-lean-4-with-harry-goldstein
Duration seconds: 2478

## Resource

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.

## Actions

- request_transcript: `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.
- read_markdown: `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.

A page view does not enqueue transcription. Agents should invoke `request_transcript` explicitly when they need this episode processed.

## Transcript

Full transcripts are not published on public pages unless there is a clear rights basis.