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

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, @oferlund and @bjoreman on Twitter, have a page on Facebook and can be emailed at info@kodsnack.se 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