Dependent types let us use the same programming language for compile-time and run-time code, and are inching their way towards the mainstream from research languages like Agda and Idris. Dependent types are useful for programming, but they also unite programming and mathematical proofs, allowing us to use the tools and techniques we know from programming to do math as well, and allowing us to run our proofs as programs.

The essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools. Dan Friedman and I have been working on a presentation of the fundamental ideas in The Little Typer, an upcoming book in the tradition of The Little Schemer. As part of the effort, we have created Pie. Pie is a little dependently typed language, small enough to understand completely but big enough to write a variety of proofs and programs.

Come get a taste of Pie, and see for yourself where dependent types can take us.