> Variables are the trickiest part of lambda calculus. And naming is the trickiest part of variables: the most complex code in our lambda evaluator is the part that renames variables to perform capture-avoiding substitutions.
> Names are artificial tedious tags whose sole purpose is to aid human comprehension. Can we get rid of them? There ought to be a way to study computation without naming names.