## Link
https://corecursive.com/021-gods-programming-language-with-philip-wadler
## Clips
### Propositions as types assures us that many aspects of programming are absolute
start = 1:50
end = 3:15
### Computer Science is a horrible name
start = 3:10
end = 4:45
### The first thing that happened in computing that convinced us there was something real here
start = 4:45
end = 6:10
### The thing the trinity discovered - Three models of computation with the exact same power
start = 6:00
end = 6:30
### The Church and Gödel story and how it showed up in a Kleene paper
start = 9:00
end = 10:00
### Kleene's paper of notes on Gödel's definition - Need to find this
start = 10:30
end = 11:30
### The impasse was resolved by Turing who wrote a whole section of his paper explaining why anything that a human computer could do can be done by a Turing machine
start = 11:00
end = 12:30
### Some people say Church's thesis should be called Turing's theorem
start = 11:45
end = 12:30
### Before incompleteness, people thought the set of things a computing machine could theoretically do was to resolve any logically well defined problem
start = 12:45
end = 13:45
### From Frege to Gödel
start = 14:30
end = 16:30
### Russell's letter to Frege and the beginning of Type Theory
start = 15:30
end = 18:30
### Beautiful story about how Frege responded to Russell's letter
start = 17:30
end = 19:00
### Godel's version of the paradoxes
start = 19:10
end = 20:30
### Gödel numbering
start = 20:30
end = 21:30
### Church proved the halting problem was unsolvable before Turing
start = 22:30
end = 23:40
### The Fixed Point Combinator or Y combinator
start = 23:50
end = 25:00
### Why incompleteness opened the door to defining computation because suddenly the problem seemed much easier
start = 25:00
end = 27:00
### Propositions as types is the generative descent of the original definition trinity
start = 28:00
end = 30:00
### The inconsistency of untyped lambda calculus
start = 30:00
end = 32:30
### The difference in the history of how types are used by the lambdas and the mus - Turing is probably the connection to the meaning of types in the mu school
start = 32:10
end = 33:30
### The meaning of type in modern functional languages is exactly the original meaning used by Church and Russell
start = 33:20
end = 34:30
### The Curry Howard correspondence was circulated in xeroxed form before finally being published in 1980 in a volume dedicated to Haskell Curry
start = 34:30
end = 36:30
### The core of the simply typed lambda calculus being at the core of every functional language is unlike anything in procedural or object oriented languages
start = 36:40
end = 38:00
### Often says lambda calculus is God's programming language, expresses the idea well despite not believing in God
start = 37:00
end = 39:45
### Maybe a better way is to say "These languages are prime"
start = 39:30
end = 40:20
### At the time he saw independence day, he had just moved to Bell Labs, and Brian Kernighan and Dennis Ritchie were his bosses
start = 41:45
end = 43:00
### Can make a good case that other intelligent species could understand a program written in lambda calculus
start = 42:30
end = 45:30
### System F - The computer science Reynolds and the logician Gerard came up with the same system at the same time in different fields
start = 48:30
end = 49:40
### Hindley Milner type system
start = 51:10
end = 51:50
### Linear Logic was first published in a computing journal - Nobody could referee it but they published it as an entire issue of the journal anyway
start = 51:50
end = 52:50
### Wadler has a huge project with government funding related to Linear Logic and communication protocols
start = 52:10
end = 53:40
### Affine logic, Relevant logic, Linear logic, all becoming more relevant in computing recently
start = 53:30
end = 56:00
### Monads came from Eugenio Moggi via Wadler - Said he doesn't understand the relationship of category theory to algebraic topology either
start = 56:00
end = 58:00
### Any interesting idea in computing has a corresponding idea in logic - There turned out to be a version of modal logic that corresponded exactly to monads
start = 57:20
end = 58:40
### Looking at logic and squinting is a great source of ideas for computing
start = 58:20
end = 59:10
### Do something good, stick with it for 30 years, and eventually some students go out and do amazing things with it
start = 58:50
end = 59:59