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
#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
#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
--------
2:23:47
#48 Bell Labs - David MacQueen
In this episode we continue with our conversation with David MacQueen, he is an Emeritus Professor from the University of Chicago, and has worked at Bell Labs for 20 years.
Bell Labs began as the research and development section of the American Telephone and Telegraph company, aka AT&T, which originally hold exclusive hold of the telephone patent. Once that expired in the 1800s they needed to develop new technology to prove that it was still the best company, and hence Bell Labs was born.
Over the course of the years this fascinating institution has registered more than 26 thousand patents, among of which we have the transistor, the laser, the solar cell and communication satellites. Over the course of the last 88 years they were awarded a jaw dropping amount of 10 Nobel prizes and 5 Turing awards.
In this interview David MacQueen shares with us how was it like to work in such an incredible institution during it’s golden age. He shares insights about the technology, the space, the people, the management style, and much more!
Links
David's Website
David's Github
--------
2:10:12
#47 The History of LCF, ML and HOPE - David MacQueen
David MacQueen has worked at Bell Labs for around 20 years during it’s Golden Age. Professor at Chicago University for 23 years. He is one of the designers of SML, one of the fathers of HOPE the programming language that introduced the notion of Algebraic Datatypes.
So this interview was very special to me personally where I could get to hear all the stories about the dawn of Functional Programming as we know. And it is my great pleasure to have the honor to share it with you all.
Links
David's Website
David's Github
Luca Cardelli and the Early Evolution of ML
The History of SML
HOPE
SML Website
SML/NJ Website
SML/NJ Github
SML Family Website
UK