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 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

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
Direct download: 612.mp3
Category:general -- posted at: 6:30am CET