Lambda calculus is omniversal
It was discovered, not invented, as shown using the Curry-Howard Correspondence between logic and programming language constructs: (25:15)
* Propositions as Types
* Proofs as Programs
* Normalization of proofs as Evaluation of programs
Curry-Howard predicts that every good idea will be discovered twice: once by a logician, and once by a computer scientist.
And pretty much ever functional language you can name has at its core the lambda calculus.
And pretty much every proof assistant you can name has at its core dependent types.
Some functional language constructs are completely arbitrary, but at there core is something that was independently discovered twice: once by a logician, and once by a computer scientist.
Not invented, but discovered.
Most of you use programming languages that were invented - and you can tell, can't you? [laughter] (27:52)
So this is my invitation to you to use programing languages that are discovered. ...
[ Why "Informatics" is a better term than "Computer Science ]
Only two things wrong with "Computer Science"
1. It's not all about computers; it's about patterns of information;
2. You don't put "science" in your name if you're a real science.