A Little Taste of Dependent Types

Explore dependent types in programming and mathematical proofs through a conference talk from Strange Loop. Dive into the world of Pie, a tiny dependently typed language featured in the upcoming book "The Little Typer." Discover how dependent types unite programming and mathematical proofs, allowing the use of familiar programming tools and techniques for mathematical reasoning. Learn about the essential beauty of dependent types, often hidden beneath layers of powerful automatic tools. Follow along as the speaker demonstrates a proof in Pie that doubles as a program, covering topics such as types and programs, addition, doubling, evidence of evenness and oddness, and the relationship between natural numbers and even/odd properties. Gain insights into the potential of dependent types and their gradual progression towards mainstream programming from research languages like Coq, Agda, and Idris.

Intro
Some Momentous Events
Types and Programs
What's a Type?
Addition
Double
There is Evidence
Evidence of Evenness
Is Zero Even?
Evidence of Oddness
All the Evidence
Every Natural Number is Even or Odd
The Step