great article! It reminds me of Curien's work on categorical combinators, where the machine definition is given by the equational axioms of the model, in this case the cartesian closed categories.
I don't think McCarthy was informed by the lambda calculus either. I've heard his background was in functional analysis and he was motivated by symbolic differentiation when inventing lisp. I'd be interested to know this history better.