Metaprogramming Your IDE in Lean 4 with Harry Goldstein

Episode 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! The Best New Programming Language is a Proof Assistant by Harry Goldstein - The Lean Programming Language - Simon Peyton-Jones: Escape from the ivory tower: the Haskell journey - "Shen: A Sufficiently Advanced Lisp" by Aditya Siram - Hypothesis Property-Based Testing library for Python -

• TigerBeetle's Spectacular Jepsen Report - with Joran Greef88 / 100
• AI & Software Quality with Shawn Wang (aka swyx)
• HTMX Creator Carson Gross on Comp Sci's Evolution
• How Mitchell Hashimoto Builds Ghostty
• Gleam's Design and Compiler - with creator Louis Pilfold