An axiom is an assumption that something is true. A theorem is a claim that something is true. A proof is a series of steps that show exactly how a theorem follows from axioms. These notions were clearly laid out in Euclid's Elements around 300 BC.
In programming, a native is a function or type provided by a compiler. A type is a claim that value of that type exist. A type-checked expression establishes that a value belongs to a type. These notions came about in the 1950's as compilers were developed.
These notions of proofs and programs turn out to correspond. This was proven by Curry and Howard from the 1930's through the 1960's, starting even before programming languages were invented.
So, why don't programmers intuitively understand this? Because, right now, it's broken in practice. Most languages have type systems that are too weak to express useful theorems, and effects systems are too permissive to typecheck proofs.
Fortunately, efforts are underway to bridge the gap. Lean (leanprover-community.github.io) has taken automated proof tools to the next level, and Idris (idris-lang.org) looks to bridge the gap. Perhaps the next mainstream programming language will complete the circuit.
• • •
Missing some Tweet in this thread? You can try to
force a refresh
