Metaprogramming Your IDE in Lean 4 with Harry Goldstein

Metaprogramming Your IDE in Lean 4 with Harry Goldstein

Author: Richard Feldman December 21, 2025 Duration: 41:18

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.


Richard Feldman hosts Software Unscripted, a weekly podcast that feels like pulling up a chair next to a fellow developer who’s seen it all. The conversations here are off-the-cuff and genuine, delving into the realities of writing code, navigating tech trends, and the often-unspoken challenges of building software. Rather than rigid interviews or dry lectures, each episode unfolds as a natural dialogue, exploring the intersection of technology, continuous learning, and the news shaping our digital tools. You’ll hear discussions that range from practical programming techniques and language debates to broader observations about the industry’s direction, all through a lens of lived experience. This isn't about polished presentations; it's about the authentic, sometimes messy, process of thinking through problems and sharing insights. For anyone who spends their days deep in logic and syntax, this podcast offers a relatable and thoughtful space to reflect on the craft. Tune in for a candid and engaging take on the world of software, one unscripted conversation at a time.
Author: Language: English Episodes: 100

Software Unscripted
Podcast Episodes
Lamdera with Mario Rogic [not-audio_url] [/not-audio_url]

Duration: 56:34
Hosted on Acast. See acast.com/privacy for more information.
Makepad with Rik Arends [not-audio_url] [/not-audio_url]

Duration: 49:10
Hosted on Acast. See acast.com/privacy for more information.