This page looks like it gives a very nice introduction to "programming" in the pure-untyped lambda calculus. But reading this, one would have no idea that a "meatier" side to lambda calculus existed. Just understanding the Church-Rosser theorem and its consequences, for example, would give a far deeper understanding than anything shown here. One thing that saddens me is that it shows construction of the combinators used to compute partial-recursive functions, but makes no discussion of the significance of this (the partial-recursive functions are an important computational class, and this is essentially a proof that they're lambda computable. Throw in a 6th type of combinator, and you've just proved lambda calculus capable of emulating one of the major models of computation).

It's certainly cool, but there's only so much to be gained from knowing that you can implement the factorial function with (λf .(λx .f (xx ))(λx .f (xx ))) (λfn.((λn.n(λu.λxy .y )(λxy .x ))n)(λfx .fx ) ((λmnf .m(nf ))n(f ((λnfx .n(λgh.h(gf ))(λu.x )(λu.u))n)))) .