4 ms·
Church's work on Lambda calculus preceded the electronic computer.
by fspeech 4y ago
Church's work on Lambda calculus preceded the electronic computer.
- pflanze 4y agoI know (although I still haven't actually read Church's work). So I know some mathematicians approached things that way. I'm just a bit puzzled that it's not the default for formalizing proofs, too. But I'll stop making conjectures now.
- fspeech 4y agoThat's because proof calculus (such as natural deduction) specifies how parts of a logic formula can be manipulated without changing its meaning. It's easier to prove and maintain the universal correctness of underlying mechanics that way. As for functional programming, ML (the Meta Language, where the object language is HOL or Higher Order Logic https://en.m.wikipedia.org/wiki/ML_(programming_language) https://en.m.wikipedia.org/wiki/ML_(programming_language) ) was created in 1973 for manipulating proofs. C was created in 1972.