Metaprogramming Your IDE in Lean 4 with Harry Goldstein

https://is1-ssl.mzstatic.com/image/thumb/Podcasts116/v4/95/3c/0a/953c0a41-0740-16ef-a95a-7790c936d06a/mza_7310709930937832253.jpg/600x600bb.jpg

Software Unscripted

Richard Feldman

114 episodes

2 weeks ago

Software Unscripted, A weekly podcast of casual conversations about code hosted by Richard Feldman.

Hosted on Acast. See acast.com/privacy for more information.

All content for Software Unscripted is the property of Richard Feldman and is served directly from their servers with no modification, redirects, or rehosting. The podcast is not affiliated with or endorsed by Podjoint in any way.

Software Unscripted, A weekly podcast of casual conversations about code hosted by Richard Feldman.

Hosted on Acast. See acast.com/privacy for more information.

Metaprogramming Your IDE in Lean 4 with Harry Goldstein

Software Unscripted

41 minutes 18 seconds

2 weeks ago

Metaprogramming Your IDE in Lean 4 with Harry Goldstein

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.