For motivation, here is an example expression from the Alligator Eggs! website:

Very briefly: A hungry alligator is an abstraction, an old (=uncolored and non-hungry) alligator can be used for bracketing, and eggs represent variables. There is an eating rule, which corresponds to beta-reduction, and a color rule for over-cautious alpha-conversion. Finally, for clean-up, there is an old age rule, which says that if a pair of parentheses contains a single term, the parentheses can be removed.
I really look forward to empirical results whether this approach helps in teaching lambda calculus.