Tuesday, January 13, 2015

Proof in Functions

Brandon Williams (tweet):

Swift’s generic functions allow us to explore a beautiful idea that straddles the line between mathematics and computer science. If you write down and implement a function using only generic data types, there is a corresponding mathematical theorem that you have proven true. There are a lot of pieces to that statement, but by the end of this short article you will understand what that means, and we will have constructed a computer proof of De Morgan’s law.


The rigorous statement of the relationship we have been grasping at is known as the Curry-Howard correspondence, first observed by the mathematician Haskell Curry in 1934 and later finished by logician William Howard in 1969. It sets up a kind of dictionary mapping terms in the computer science world to terms in the mathematics world.

Update (2015-01-24): [Solutions to Exercises] “Proof in Functions”.

Comments RSS · Twitter

Leave a Comment