I agree. One problem is simply that the notation is linear, while lambda calculus is inherently hierarchical. That problem affects all programming languages to

I agree. One problem is simply that the notation is linear, while lambda calculus is inherently hierarchical. That problem affects all programming languages to some degree, but it is particularly damaging to the comprehension of lambda terms. Another problem is the complications that are introduced by giving names to variables. This has actually been discussed quite a bit in literature. For example, that the term "λx.xx" is alpha equivalent to "λy.yy", simply means that the language has redundancy. In fact "alpha equivalence", "unbound variables", and "capture avoiding substitution", are all concepts made necessary by the use of names. If you refuse to name terms, the calculus becomes conceptually simpler. This isn't a revalation by any means. Church pointed this out. It just happens that naming things is a very useful thing to do when writing proofs. So we kind of just have to deal with it. Point-free reasoning is a good way to avoid some of these complications, which contributes to the popularity of combinator calculi like SKI when teaching untyped lambda calculus. Another way is to use a graphical representation to depict variable binding more explicitly. See examples below: * http://dkeenan.com/Lambda/ http://dkeenan.com/Lambda/ * https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html * http://bntr.planet.ee/lambda/work/visual_lambda.pdf http://bntr.planet.ee/lambda/work/visual_lambda.pdf