I mean, a really solid understanding of substitution is probably one of
the major contributions of lambda calculus. For what's effectively an implementation to get that wrong is pretty pathological. And also, there's no reason to defend it. It's a bug. Period. Yet here we are.
And there's a whole hell of a lot more in the world than software development...
To the extent that lisp captures any of these other foundational ideas/theories/techniques, type theory does better (which is what I was pre-empting with my original reference, not the role of type systems in the world of practical software development).