Propositions as “Types” by Philip Wadler 2015

Programming languages which are discovered (man-made) are Functional Programming (Lisp, Haskell, Scala, ML,… ) using “Propositional Logic” (Typed Lambda Calculus).

Note: Java, C++, Python are invented, not discovered!

Ref: Curry Howard Lambek Isomorphism: they are all the same thing with different ‘faces’ :

“Logic = Algebra = Lambda-Calculus = Category = Type”

Notes: Layman’s terms equivalent:

  1. Isomorphism = Same = Congruence
  2. Homomorphism = Similar
  3. Proposition = Claim / Fact


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s