There is one very practical use of the lambda calculus (and related calculi), which is to check whether your language implements the logic of functions correctl

There is one very practical use of the lambda calculus (and related calculi), which is to check whether your language implements the logic of functions correctly. For example, does your language support a polymorphic identity function, and if so, what happens when you apply a polymorphic identity function to a polymorphic identity function? What _should_ happen is easy to check in the lambda calculus, but it’s easy to not think this all the way through in an interpreter or compiler implementation. Rewriting is a pretty slow evaluation procedure, so we often using a machine’s native call stack instead, but doing so can get us in trouble. Functions in plenty of languages do not work as the lambda calculus suggests they should, and those languages are mostly fine, but when user code gets dicey, they can operate in surprising and counterintuitive ways. What I like about the lambda calculus is that it captures, in an unbelievably small package, many of the things that we intuitively want a language to do.