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)))) .
I also think this article is lacking. Something also about domain[1] theory and categorical models could be discussed. Particular the latter as they relate to abstract machines, .eg. Curien's thesis work on combinators and functional programming. I'm not saying one can explore these in depth, but at least throw them out there for further reading to help provide a roadmap for the "meatier" side.
One could also cite a few programming constructs, .eg. (let (... and show how lisp is essentially syntactically sugared lambda calculus.
I should also add Carl Gunter's excellent "Semantics of Programming Languages: Structures and Techniques", as a good intro to this area.
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)))) .