The 1925 publication of Principia Mathematica caused something of a stir in academic circles back then. By firmly vesting precise mathematical notation and insisting on the precise use of language, Betrand Russell and Alfred Whitehead convinced approximately everybody in science and mathematics that it was time to stamp out ambiguity in scientific claims. Expressions and symbols like this became commonplace: φx ≡x ψx .⊃. (x): ƒ(φẑ) ≡ ƒ(ψẑ).
The year 1925 precedes a lot of change that has hit the world since then. The most important change is the advent and widespread use of computing devices, that is, computers.
One problem that we have run into is that a mathematical problem phrased in the Russell-Whitehead notation is not particularly well executable on a computing device. Besides making a particular, precise claim, the Russell-Whitehead notation does not allow you to verify it on a computer. That characteristic of the Russell-Whitehead approach is not particularly efficient. I will show in this blog post why it is even dangerous.
The Curry-Howard correspondence, on its side, claims that every mathematical “proof” is a program and the other way around. Therefore, instead of using a non-executable notation for “proof”, it should always be possible to use an executable one.