I'm just reading up on lambda calculus to get to know it. I see it as an alternate form of computation as opposed to the Turing Machine. It's an interesting way of doing things with functions/reductions (crudely speaking). Some questions keep nagging at me though: What's the point of lambda calculus? Why go through all these functions/reductions? What is the purpose?As a result I'm left to wonder: What exactly did lambda calculus do to advance the theory of CS? What were it's contributions that would allow me to have an aha moment of understanding the need for its existence?Why is lambda calculus not covered in texts on automata theory? The common route is to go through various automata, grammars, Turing Machines and complexity classes. Lambda calculus is only included in the syllabus for SICP style courses (perhaps not?). But I've rarely seen it be a part of the core curriculum of CS. Does this imply it's not all that valuable? Maybe not and I maybe missing something here?I'm aware that functional programming languages are based on lambda calculus but I'm not considering that as a valid contribution, since it was created much before we had programming languages. So, really what is the point of knowing/understanding lambda calculus, w.r.t. its applications/contributions to theory?
What is the contribution of lambda calculus to the field of theory of computation?
soft question;big picture;lambda calculus;ho.history overview
$\lambda$-calculus has two key roles.It is a simple mathematical foundation of sequential, functional, higher-ordercomputational behaviour.It is a representation of proofs in   constructivelogic.This is also known as the Curry-Howard correspondence.  Jointly,the dual view of $\lambda$-calculus as proof and as (sequential,functional, higher-order) programming language, strengthened by the algebraic feelof $\lambda$-calculus (which is not shared by Turing machines), has leadto massive technology transfer  between logic, the foundations of mathematics, and programming.This transfer is still ongoing, for example in homotopy type theory.  Inparticular the development of programming languages in general, andtyping disciplines in particular, is inconceivable without$\lambda$-calculus. Most programming languages owe some degree of debt toLisp and ML (e.g. garbage collection was invented for Lisp), which are direct descendants of the $\lambda$-calculus. Asecond strand of work strongly influenced by $\lambda$-calculus areinteractive proof assistants.Does one have to know $\lambda$-calculus to be a competent programmer, oreven a theoretician of computer science?    No. If you are not interestedin types, verification and programming languages with higher-orderfeatures, then it's probably a model of computation that's notterribly useful for you. In particular, if you are interested in complexity theory, then$\lambda$-calculus is probably not an ideal model because the basicreduction step $$(\lambda x.M) N \rightarrow_{\beta} M[N/x]$$ is powerful: it can make an arbitrary number of copies on $N$, so$\rightarrow_{\beta}$ is an unrealistic basic notion in accounting forthe microscopic cost of computation. I think this is the main reason whyTheory A is not so enamoured of $\lambda$-calculus. Conversely, Turing machines are not terribly inspirational for programming language development, because there are no natural notions of machine composition, whereas with $\lambda$-calculus, if $M$ and $N$ are programs, then so is $MN$. This algebraic view of computation relates naturally to programming languages used in practice, and much language development can be understood as the search for, and investigation of novel program composition operators.For an encyclopedic overview of the history of $\lambda$-calculus see History of Lambda-calculus and Combinatory Logic by Cardone and Hindley.