Why the work of two different mathematicians trying to lay the foundations for mathematics ended up being directly used to program computers? How programming and constructive logic are tied together and can be seen as two sides of the same coin? How a theory created to overcome the paradoxes of set theory is fundamental to programming and used to write better behaved programs? Why a branch of abstract math invented to justify natural transformations is very popular with (functional) programmers?

We often use programming to solve math problems, but … what if we use math to solve programming problems?

Is programming… math?

Let’s take a tour through lambda calculus, the Curry-Howard equivalence, and category theory, and explore the relationship of math and programming, particularly in functional programming and the rich span of possibilities that this relationship entails and why that matters.