{"podcast":{"title":"Software Unscripted","slug":"software-unscripted-5320480","podcast_index_feed_id":5320480,"rss_url":"https://feeds.acast.com/public/shows/664fde3eda02bb0012bad909","website_url":"https://feeds.acast.com/public/shows/software-unscripted","image_url":"https://assets.pippa.io/shows/664fde3eda02bb0012bad909/show-cover.jpg","author":"Richard Feldman","episode_count":119,"summary":"Software Unscripted, A weekly podcast of casual conversations about code hosted by Richard Feldman. Hosted on Acast. See acast.com/privacy for more information.","last_synced_at":"2026-06-20T20:20:49.192637+00:00","page_url":"https://stenobird.com/podcast/software-unscripted-5320480"},"episode":{"title":"Metaprogramming Your IDE in Lean 4 with Harry Goldstein","slug":"metaprogramming-your-ide-in-lean-4-with-harry-goldstein","published_at":"2025-12-21T20:18:10+00:00","page_url":"https://stenobird.com/podcast/software-unscripted-5320480/metaprogramming-your-ide-in-lean-4-with-harry-goldstein","show_page_url":"https://stenobird.com/podcast/software-unscripted-5320480","url":"https://shows.acast.com/software-unscripted/episodes/metaprogramming-your-ide-in-lean-4-with-harry-goldstein","audio_url":"https://sphinx.acast.com/p/open/s/664fde3eda02bb0012bad909/e/69485602f7567117397e5223/media.mp3","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.","meta_description":"Harry Goldstein talks with Richard Feldman about the Lean 4 programming language's compile-time metaprogramming capabilities, including how they can be us…","key_points":[],"chapters":[],"topics":[],"duration_seconds":2478,"processing_state":"not_requested","actions":[{"name":"request_transcript","method":"POST","url":"https://stenobird.com/v1/public/podcasts/software-unscripted-5320480/episodes/metaprogramming-your-ide-in-lean-4-with-harry-goldstein/transcription-requests","description":"Idempotently request low-priority transcript generation for this episode."},{"name":"read_markdown","method":"GET","url":"https://stenobird.com/podcast/software-unscripted-5320480/metaprogramming-your-ide-in-lean-4-with-harry-goldstein.md","description":"Read the agent-friendly Markdown representation of this episode resource."}]}}