February 24, 2020

Propositions as Types


Philip Wadler, computer scientist contribs to Programming Language Design and Type Theory


Very rigorous field of study. His point about if mathematics is discovered or invented is something astonish. I had this discussion with a friend back at the university days and we reach obviously no conclusion. But isn’t that odd that both Leibniz and Newton came to the same definition of what Calculus must be like?

They can’t both invent something equivalent out of nowhere.

Now in this talk there are many evidences that logicians and computer scientists they are discovering the same patterns under different terminologies.


Logic is complete. Every provable statement is true and every true statement is provable.

The difference between Turing’s solution was only in philosophy.

Lamba is omniversal!

How information is structure goes by the name of Informatics. There are only two things wrong with Computer Science, the word Computer and the word Science. First because it is not only about computers and second because you don’t put science in the name if you are a real science.


  1. Is mathematics invented or discovered? Seems like discovering for me.

  2. Propositions in logic corresponds to types

  3. Proofs in logic corresponds to programs

  4. Simplification of proofs in logic corresponds to evaluation in programs

  5. Use programming languages that are discovered and not invented!

Tags: theory functional