#53 RustBelt, Iris, and the Art of Writing - Derek Dreyer
Derek Dreyer is a professor at the Max Planck Institute, in 2024 he was awarded the ACM Fellowship, in 2017 he got the ACM Sigplan Robin Milner Young Researcher Award. And has participated or lead greatly influential work, such as the RustBelt Project and Iris.
In this episode Derek shares his experience going to Grad School at CMU, how even a great research as himself has fallen pray to the impostor syndrome and how to cope with it. Throughout the conversation he makes beautiful parallels between music and academic papers, and how the work of a researcher is similar to that of an artist an many aspects. He also gives us a few tips about how to become a better academic writer. And of course, we also talked about Rust and the history about formally verifying its type system.
Don't forget to check our merch store!
Links
Derek's Website
POPL '25 PLMW Talk - How to Read Papers so that People Can Read Them
--------
2:25:22
--------
2:25:22
#52 Why is Haskell so special - Lennart Augustsson
Lennart Augustsson has spent the last four decades quietly — and sometimes mischievously — shaping the way we think about code.
He co-authored Lazy ML in the early 80s, wrote A Compiler for LML back in 1984, and was behind HBC, the first publicly available Haskell compiler.
If you've used Haskell, worked with hardware described in Bluespec, or played around with weird combinator-based toy languages, there's a decent chance you've crossed paths with his ideas — directly or indirectly.
He's also won the International Obfuscated C Code Contest — not once, but multiple times — reminding us that playfulness and rigor aren't mutually exclusive.
But his work didn't stop in academia or hobby projects. He’s brought functional programming into finance, hardware design, large-scale industry — with stints at Credit Suisse, Facebook, Google, and now Epic Games, where he’s helping design a new functional logic programming language called Verse.
Over the course of this conversation, we’ll talk about lazy evaluation, type theory, programmable dungeons, the compromises of real-world programming, and what it means to still be building languages after 40 years in the game.
Links
Type Theory Forall Merch Store
Ko-Fi
Discord Server
Haskell Interlude
Lennart's Wikipedia Page
Lennart's Webpage
--------
1:30:31
--------
1:30:31
#51 s/Coq/Rocq - Nicolas Tabareau
In this episode we talk with Nicolas Tabareau, the Head of Gallinette, one of the main teams which develop the Rocq theorem Prover at Inria.
The original idea of this interview is to talk about the rebranding from Coq into Rocq, which is very exciting to our community. However, Nicolas has such a prolific research career that I couldn’t miss the opportunity to get him to talk so much more about it.
So in this conversation we talk about his early publications in neuroscience, his views on Category Theory applied to Type Theory, Rocq’s rebranding, and the institution around it, MetaRocq and the conceptual boundaries of certifying a theory inside itself. Of course we wouldn’t miss the opportunity to also discuss how Rocq view the growing influence that Lean is gaining in our community.
Links
Type Theory Forall Store
Type Theory Forall Website
Nicolas Tabareau Website
MetaRocq Github
--------
1:42:05
--------
1:42:05
#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra
Wouter Swierstra is a Math Bachelor’s from the University of Utrecht, has done his PhD with Thorsten Altenkirch at the University of Nottingham, did a post-doc at Chalmers, has experience in the industry working on facilitating the design of embedded system using FP and currently is a Professor at the University of Utrecht and co-host of the Haskell Interlude Podcast.
In this episode we talk about his trajectory into formal methods and functional programming. We talk about Datatypes a la Carte, the Expression Problem, Functional Pearls, Program Synthesis vs Program Calculation, and much more!
0:00 – Intro & Welcome
0:02:08 – Announcing the Type Theory Forall Merch Store!
1:12 – Early Influences: From Lenses to Logic
4:40 – Discovering Functional Programming in Utrecht
8:15 – On Monads, Papers, and Learning by Teaching
12:20 – What Makes a Paper ‘Beautiful’?
17:50 – PhD in Nottingham: Theory Meets Community
22:00 – Writing ‘Certified Programming with Dependent Types’
29:10 – Teaching Dependent Types: Challenges and Joys
34:00 – On Agda vs Coq: Philosophies and Use Cases
38:40 – Type-Driven Development in Practice
45:05 – The Power of Elegant Proofs
52:00 – Advice to Aspiring Researchers in Type Theory
1:03:00 – Beating C with Functional Programming
1:20:00 – Formal Verification and Loop Invariants
1:33:28 – Program Calculation vs Program Synthesis
1:39:00 – Formalizing Blockchain
2:01:38 – Final Thoughts
Links
Wouter Website
Haskell Interlude
Advanced FP Summer School
ttforall twitch
ttforall store
Discount code for 10% off: typetheory
--------
2:06:47
--------
2:06:47
#49 Self-Education in PL - Ryan Brewer
Ryan Brewer is a college dropout who has an incredible blog about PL, Category Theory and Logic. He better define his goal as making Formal Theory more accessible outside the ivory tower of academia, and easier to put into practice where it matters.
He has a couple of very interesting main projects, such as the first Cedille 2 Interpreter, Saber VM, and Arctic.
In this episode we will talk about all of his projects. His trajectory becoming self-taught in PL, compilers and Formal Methods, and he shares with us the wealth of resources he used to navigate this sea of knowledge. We also have a brief but heated discussion on the ethics of Science.
0:00 – Intro & Podcast Community
3:40 – How Ryan Started Learning Programming Languages
12:40 – Projects, Category Theory & Early Experiences
18:00 – College Life, Dropping Out & Study Strategies
27:00 – Landing a Developer Job Without a Degree
32:00 – Thoughts on JavaScript, TypeScript & WebAssembly
37:00 – Building Arctic: A Compiler for Blogs
41:00 – Introduction to Gleam & Its Unique Features
48:00 – Functional Programming at Work & Community Impact
59:00 – Diving into Haskell and Category Theory
1:08:30 – Ethical Considerations in Software Licensing
1:20:00 – Reflections on Academia & Learning
1:32:30 – Job Interviews & Practical Programming Tools
1:38:00 – Dan on Academia and Podcasting Philosophy
1:54:00 – Final Reflections & Advice for Self-Learners
2:05:00 – Closing Thoughts, Blog, Open Source
2:19:58 – Outro
Links
Ryan's Website
Saber VM
Arctic, which is built on top of Lustre
Category Theory Wiki
USA