Metaprogramming Your IDE in Lean 4 with Harry Goldstein
About this episode
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.
Get every episode summarized
Each time Software Unscripted publishes, we email you a written briefing from the transcript — the topics, who appeared, and any specific claims, with the ad reads skipped.
Email me new episodesFree for 3 shows. No card needed.
Hosts & guests
No transcript yet
This episode has not been transcribed. Request it and it moves to the front of the queue.
More episodes
More from Software Unscripted
Fast Functional Reactive Programming with Datastar Creator Delaney Gillilan
Software Unscripted
TigerBeetle's Spectacular Jepsen Report - with Joran Greef
Software Unscripted
AI & Software Quality with Shawn Wang (aka swyx)
Software Unscripted
HTMX Creator Carson Gross on Comp Sci's Evolution
Software Unscripted