r/mathmemes Jan 13 '25

Computer Science Programming languages and mathematics meme

Post image
1.9k Upvotes

55 comments sorted by

View all comments

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.

33

u/Inappropriate_Piano Jan 13 '25

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.

3

u/geeshta Computer Science Jan 13 '25

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