Show Notes
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.
More from Software Unscripted
Casey Muratori talks with Richard about Casey's 2025 talk "The Big OOPs" about the history of Object-Oriented Programming, as well as performance, architecture, software quality, and plenty of other topics.
Richard talks with Datastar creator Delaney Gillilan about fast functional reactive programming, how Datastar outcompetes more mainstream JavaScript libraries on performance, and how he designed it - including how Richard's book Elm in Action turned out to be one of its sources of inspiration.
Richard talks with TigerBeetle founder Joran Greef about how their team's database achieved a wildly successful Jepsen Report. Where other databases have been famously skewered in the past, TigerBeetle passed with flying colors, and Richard and Joran discuss the story of how they got there, how TigerBeetle makes money when their database is open source, and many other topics around software quality in general.
Richard talks with AI expert Shawn "swyx" Wang about all sorts of AI topics, including how it fits into IDEs, AI agent implementations, the economics of AI subscriptions, the future of AI in software, and how all of this affects software quality.
HTMX creator and Montana State University instructor Carson Gross talks to Richard about why HTMX moved from version 2 straight to version 4, API boundaries in library design, jQuery, and how the field of Computer Science education is now changing from the perspective of someone who's been teaching it for years.