Are Programmers Philosophers in Disguise?
The Curry-Howard correspondence for beginners
What do programming and philosophy have in common? A lot more than you think. This article will explain, in beginner-friendly terms, exactly how that relationship looks and how it was discovered. I’ll break down this concept into four sections:
· Logic: the Key to Philosophy and Programming
· Propositions as Types
· Proofs as Programs
· What it Means for Programmers
Logic: The Key to Philosophy and Programming
The key piece in connecting philosophy and programming is logic. In the fourth century BCE, Aristotle created a kind of logic that would form the foundation for all logic to follow, built on propositions and conclusions.
Proposition: All men are mortal.
Proposition: All greeks are men.
Conclusion: All greeks are mortal.
Propositions are facts that we propose are true, and the conclusions we can conclude to be true after considering all the propositions together.
Over the following centuries, these ideas would be built on and evolve into new kinds of logic, allowing for more sophisticated propositions and conclusions to be made and eventually creating modern mathematics as we know it today.
In the 1930s, logic continued to evolve, but a new area of science was now being explored: computer science. Over the next 30 years, two scientists would come to a conclusion that would forever change math and computer science:
Mathematical logic and computer programs are equal!
These two individuals were the mathematician Haskell Curry and the Logician William Alvin Howard, and their discovery is named the Curry-Howard-Correspondence.
So, what exactly is the Curry-Howard correspondence and how does it tell us that logic and programs are equal? To answer this question, we’ll look at two relationships: propositions and types and proofs and programs.
Propositions as Types
Logical propositions allow us to state knowledge about the world around us, and proofs tell us whether or not that knowledge is accurate. The Curry-Howard correspondence tells us that we can also state that knowledge with computer types and prove it using computer programs. To demonstrate this in action, consider this simple math problem:
Hello + 5 = ?
If you think this is a silly question, you’re right! But why doesn’t it make sense? Well, when we use the + symbol, we expect to add together two numbers, and the word “hello” is not a number. We might state this with a logical proposition saying:
For any two things being added together, those two things are numbers.
The Curry-Howard correspondence tells us we can say the same thing using types. In this case, we’re giving the type of the addition function.
The addition is a function that takes two numbers as input and returns a new number as output.
Function Plus
Input : Number, Number
Output : NumberThis is called the function’s type signature — it identifies the function, just as your signature would identify you.
So, now that we have our logical proposition and our computer type, we can use the Curry-Howard correspondence to show that hello + 5 doesn’t make sense with logical proof and a computer program.
Proofs as Programs
Let’s start with the logical side:
For any two things being added together, those two things are numbers.
In our example of hello + 5, we have two things being added together:
- “hello”
- 5
Our proposition tells us that both of the things being added together are numbers, and our statement tells us something different: that only one of them is a number — which is logically inconsistent.
So, we’ve used logic to show why our statement doesn’t make sense — now we can use a computer program to do the same thing.
Remember our function has this type signature:
Function Plus
Input : Number, Number
Output : NumberSo, what happens when we try our function with our inputs of hello and 5?
> Hello + 5
Type Error: Expected type "Number", recieved type "String"Our program fails to run, giving us a type error. Before trying to add together our inputs, the computer checked the types of the inputs. We call this type-checking, and it ran into a problem: it failed to type-check.
So, both logic and the computer told us hello + 5 doesn’t make sense with a logical inconsistency and a type error. With the Curry-Howard correspondence, we know this isn’t a coincidence and that, in fact, the logic and the program are doing the same thing.
What It Means for Programmers
While showing that hello + 5 doesn’t make sense isn’t exactly a revolutionary result. The Curry-Howard correspondence is critical to research in programming and philosophy.
The Curry-Howard correspondence allows computer scientists, mathematicians, and philosophers to use the same language and work together to make new software, theories, and frameworks.
When types, logical theories, and programs become more complex, the implications of the Curry-Howard correspondence can be used to create sophisticated models and prove the properties of programs.
Learning the foundations of computer science is important to becoming a better programmer. If you want to learn more about these fundamental computer science concepts in a beginner-friendly way, stay tuned for my future articles covering type theory and functional programming.
