#28 Formally Verifying Smart Contracts
February 15th 2023
Pruvendo
#27 Formalizing an OS: The seL4
February 4th 2023
Gerwin Klein
#26 Mechanizing Modern Mathematics
January 16th 2023
Kevin Buzzard
#25 Formally Verifying the Tezos Codebase
November 21st 2022
Formal Land
#24 The History of Isabelle
October 6th 2022
Lawrence Paulson
#23 What is the SIGPLAN?
September 23th 2022
Jens Palsberg and Jonathan Aldrich
#22 Impredicativity, LEM, Realizability and more
August 12th 2022
Cody Roux
#21 Denotational Design
August 4th 2022
Conal Elliott
#20 Huaweii, String Diagrams, Game Semantics
June 27th 2022
Dan R. Ghica
#19 Experience Report: Learning Coq
June 4th 2022
Patrick and Supun
#18 Gödel's Incompleteness Theorems
May 19th 2022
Cody Roux
#17 The Lost Elegance of Computation
May 9th 2022
Conal Elliott
#16 Agda, K Axiom, HoTT, Rewrite Theory
April 2nd 2022
Jesper Cockx
#15 Coq Projects, Agda, Idris, Kind
March 27th 2022
Nitin and Eric
#14 POPL, Parametricity, Scala, DOT
February 12th 2022
Nitin and Eric
#13 C/C++, Emacs, Haskell, and Coq. The Journey
December 23rd 2021
John Wiegley
This episode is about the journey of a programmer that converted himself into a Haskell developer after working with C/C++ for more than 10years.
Here are a few questions that you’ll find the answer to in this episode:
- What does he find so compelling about Haskell?
- Why did it make him dive deeper into the Theoretical Computer Science?
- Why did it make him learn Coq and Category Theory?
- How does Coq compare with ACL2?
- How do both Coq and ACL2 compares to TLA+?
- Did learning Coq make John a better programmer?
Links
- John’s Email: johnw@newartisans.com
- John’s Twitter: @jwiegley
Tweet
