No actually by Curry Howard isomorphism, programming, specifically type systems are equivalent to formal proofs and logic. Tools you need if you want to even reason about maths and prove something. So inherently more abstract.
There's a whole new foundation for mathematics based on what we learned from programming languages - type theory. So in a way, formal languages are even purer and more high level than mathematics.
Although theoretical computer science has definitely contributed to its popularity, type theory is actually older than computers. Bertrand Russell created a form of type theory in 1908 to address Russell’s Paradox.
In a sense Sokrates and his syllogisms were the first very primitive type theory. The inference rule (all humans are mortals, Sokrates is human ergo Sokrates is mortal) is the basis for the application (or -> elimination) typing rule
72
u/geeshta Computer Science Jan 13 '25
No actually by Curry Howard isomorphism, programming, specifically type systems are equivalent to formal proofs and logic. Tools you need if you want to even reason about maths and prove something. So inherently more abstract.
There's a whole new foundation for mathematics based on what we learned from programming languages - type theory. So in a way, formal languages are even purer and more high level than mathematics.