
Picture Me Coding
Picture Me Coding is a music podcast about software. Each week your hosts Erik Aker and Mike Mull take on topics in the software world and they are sometimes joined by guests from other fields who arrive with their own burning questions about technology.
Email us at: podcast@picturemecoding.com
Patreon: https://patreon.com/PictureMeCoding
You can also pick up a Picture Me Coding shirt, mug, or stickers at our Threadless shop: https://picturemecoding.threadless.com/designs
Logo and artwork by Jon Whitmire - https://www.whitmirejon.com/
Picture Me Coding
Gleaming the Lambda Cube with Nathan Mull
This week Nathan Mull, a type theorist and CS Professor at Boston University, came on the show to help Mike and Erik understand what the phrase "Propositions as Types" is all about. This is an idea about how programs are connected to logic and mathematical proofs, whether we want them to be or not! You know that program that orders pizza from Dominos?! Yes, even that program is a proof of something. Find out what it proves on this episode of Picture Me Coding!
Links
- Nathan Mull's personal site
- 2014 Philip Wadler Paper: Propositions as Types
- 2016 Strangeloop Conference recording (Youtube): "Propositions as Types" by Philip Wadler