Propositions as Types
Youtube Link
Speaker
Philip Wadler, computer scientist contribs to Programming Language Design and Type Theory
Thoughts
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.
Quotes
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.
Recommendations

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

Propositions in logic corresponds to types

Proofs in logic corresponds to programs

Simplification of proofs in logic corresponds to evaluation in programs

Use programming languages that are discovered and not invented!
Books

An unsolvable problem of elementary number theory  by Alonzo Church

General recursive functions of natural numbers  by Kurt Godel

On computable numbers, with an application to the Entscheidungsproblem  by Alan Turing

Natural Deduction  by Gerhard Gentzen (1935)