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.

• Type Theory Forall Store
• Type Theory Forall Website
• Nicolas Tabareau Website
• MetaRocq Github

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

• Wouter Website

• Haskell Interlude

• Advanced FP Summer School

• ttforall twitch

• ttforall store

Discount code for 10% off: typetheory

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

• Ryan's Website
• Saber VM
• Arctic, which is built on top of Lustre
• Category Theory Wiki