Kodsnack 612 - Where types first come in, with Pedro Abreu

Kodsnack

Fredrik talks to Pedro Abreu about the magical world of type theory. What is it, and why is it useful to know about and be inspired by?

Pedro gives us some background on type theory, and then we talk about how type theory can provide new ways of reasoning about programs, and tools beyond tests to verify program correctness. This doesn’t mean that all languages should strive for the nirvana of dependent types, but knowing the tools are out there can come in handy even if the code you write is loosely typed.

We wrap up with some further podcast tips, of course including Pedro’s own podcast Type theory forall.

Thank you Cloudnet for sponsoring our VPS!

Comments, questions or tips? We a re @kodsnack, @tobiashieta, @oferlundand @bjoreman on Twitter, have a page on Facebook and can be emailed at [email protected] if you want to write longer. We read everything we receive.

If you enjoy Kodsnack we would love a review in iTunes! You can also support the podcast by buying us a coffee (or two!) through Ko-fi.

Links

• Pedro
• Type theory
• Type theory forall - Pedro’s podcast
• Chalmers
• The meetup group through which Pedro and Fredrik met
• Purdue university
• Bertrand Russell
• The problem of self reference
• Types
• Set theory
• Kurt Gödel
• Halting problem
• Alan Turing
• Turing machine
• Alonzo Church
• Lambda calculus
• Rust
• Dependent types
• Formal methods
• Liquid types - Haskell extension
• SAT solver
• Property-based testing
• Quickcheck
• Curry-Howard isomorphism
• Support Kodsnack on Ko-fi!
• Functional programming
• Imperative programming
• Object-oriented programming
• Monads
• Monad transformers
• Lenses
• Interactive theorem provers
• Isabelle
• HOL
• Dafny
• Saul
• Crucible
• Symbolic execution
• CVC3, CVC5 solvers
• Pure functions
• C#
• Algebraic data types
• Pattern matching
• Scala
• Recursion
• Type theory forall episode 17: the first fantastic one with Conal Elliot. The discussion continues in episode 21
• Denotational types
• Coq
• IRC
• Software foundations - about Coq and a lot more
• The church of logic podcast
• The Iowa type theory commute podcast

Titles

• Type theory podcasts
• Very odd for some people
• Brazilian weather
• Relearning to appreciate
• The dawn of computer science
• Layers of sets
• Where types first come in
• Bundle values together
• The research about programming languages
• If you squint your eyes enough
• Nirvana of type systems
• Proofs all the way down
• Extra guarantees
• If your domain is infinite
• Formal guarantees
• The properties of my system
• What is the meaning of my program?
• Building better systems