Formal Logic Undressed — Paul Snively

You may have heard of the Curry-Howard Isomorphism and that it relates types and logic. But isn’t logic just Boolean algebra? And haven’t there been many, maybe even most, times when types didn’t have anything to do with the problem you were trying to solve, at best, and just got in the way, at worst? What’s the big deal?

In this workshop, we’ll dig into the basics of what we mean by “logic” in the context of, but also short of, the Curry-Howard Isomorphism. We’ll spend some time visiting Raymond Smullyan’s islands of Knights and Knaves, where Knights always tell the truth and Knaves always lie.

We’ll cheat a little bit by packing laptops loaded up with Coq and PeaCoq in our backpacks. We’ll learn a little bit about some of the Great British contributors to the field of formal logic — Boole, de Morgan, Carroll. We’ll return from the Islands of Knights and Knaves to the Lake District and see how some of these lessons apply to Scala. And we’ll have fun doing it.