I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which strives to answer the question of "computability" i.e., things that can/cannot be computed with various constraints, I'm struggling to find the analog for "Theory of Programming"
Wikipedia describes it as:
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features.
This is like saying "everything" which isn't really specific.
The common progression of the topics is usually like so:
Combinatory Logic > Lambda Calculus > Martin Lof Type Theory > Typed Lambda Calculus > (Something happens here) > Programming languages developed - that have very little connection with CL/$\lambda$
I can see the underlying "math" involved with CL/$\lambda$ and interesting proofs that come out as a result including the Church-Rosser theorem and that's neat. However, I'm struggling to understand the "end goal" of all this undertaking? What's the holy grail of PLT if you will? For now it seems to just be scratching an intellectual itch but I can't really cross the bridge from research/theory to anything practical.
Note: I do get it up until using the $\lambda$-calc for undecidability proofs. But beyond its applicability to "computability" I just don't get it and am having a hard time even understanding the need for research in PLT from this narrow POV. Any existing books, references that can throw light on the "big picture" of PLT?