Metaprogramming Your IDE in Lean 4 with Harry Goldstein
Software Unscripted21 Joulu 2025

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.

Jaksot(117)

HTMX Creator Carson Gross on Comp Sci's Evolution

HTMX Creator Carson Gross on Comp Sci's Evolution

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 fiel...

1 Huhti 1h 27min

How Mitchell Hashimoto Builds Ghostty

How Mitchell Hashimoto Builds Ghostty

Ghostty creator and Hashicorp cofounder Mitchell Hashimoto talks with Richard about the development of that high-performance terminal emulator: how he's been building Ghostty, how he does native GUI d...

17 Helmi 1h 3min

Gleam's Design and Compiler - with creator Louis Pilfold

Gleam's Design and Compiler - with creator Louis Pilfold

Gleam programming language creator Louis Pilfold talks with Richard about Gleam's design and various challenges that came up when implementing its compiler.- Gleam Language - https://gleam.run- Erlang...

10 Tammi 1h 11min

Jonathan Blow on Programming Language Design

Jonathan Blow on Programming Language Design

Jonathan Blow, creator of popular games Braid and The Witness, talks with Richard about programming language design - including the design of the programming language he's been building for game devel...

15 Marras 20251h 41min

Zig Creator Andrew Kelley

Zig Creator Andrew Kelley

Richard talks with Zig Creator Andrew Kelley.- Support Zig - https://ziglang.org/zsf/- Zig's "Writergate" - https://ziglang.org/download/0.15.1/release-notes.html#Writergate- "What Color is Your Funct...

9 Loka 20251h 49min

Securing Evolving Software with Noah Hall

Securing Evolving Software with Noah Hall

xz vulnerability: https://en.wikipedia.org/wiki/XZ_Utils_backdoorSpectre: https://en.wikipedia.org/wiki/Spectre_(security_vulnerability)Meltdown: https://en.wikipedia.org/wiki/Meltdown_(security_vulne...

20 Syys 202559min

Andreas Kling on Ladybird Browser, SerenityOS, and Powerlifting

Andreas Kling on Ladybird Browser, SerenityOS, and Powerlifting

Ladybird Browser - https://ladybird.orgSerenityOS - https://serenityos.orgStory of the man who used powerlifting to recover after falling off a roof https://startingstrength.com/articles/brian_jones_s...

1 Syys 20251h 20min

Suosittua kategoriassa Politiikka ja uutiset

uutiscast
aikalisa
politiikan-puskaradio
ootsa-kuullut-tasta-2
rss-ootsa-kuullut-tasta
tervo-halme
rss-podme-livebox
rss-vaalirankkurit-podcast
rss-asiastudio
otetaan-yhdet
rss-raha-talous-ja-politiikka
the-ulkopolitist
et-sa-noin-voi-sanoo-esittaa
rss-sinivalkoinen-islam
rss-hyvaa-huomenta-bryssel
aihe
rss-polikulaari-pitka-kiekko-ja-muut-ts-podcastit
rss-girls-finish-f1rst
rss-kovin-paikka
rss-tasta-on-kyse-ivan-puopolo-verkkouutiset