> The point is that rust already feels like being thrown into the deep end of the pool, and all the lambda calc is as deep if not deeper. I don't think you nee

> The point is that rust already feels like being thrown into the deep end of the pool, and all the lambda calc is as deep if not deeper. I don't think you need an undergraduate degree to understand the un-typed lambda calculus. You can build an intuition for it with syntactic substitution at first. For such a big idea it's really quite simple in practice. That makes it quite beautiful. Moving to the typed lambda calculus is the next step and builds upon the prior knowledge. The reason I think it's useful is that it allows you to reason about abstractions -- even complicated ones -- in a manner that reduces the cognitive burden on us. It's also not tied to any single programming language: they can all be modeled with mathematics. Proofs are programs and programs are proofs. I do agree that a hefty does of practical application helps to solidify theoretical understanding. I see them as informing one another.