> The quotes from Church and Gödel are saying that Turing's formalism was the more helpful in making the case that it had captured the notion of effective calculability. That's understandable - it's much like e.g. Cantor's diagonal, in that it makes its subject very concrete.

This is what I primarily meant with my controversial statement, sorry I didn’t articulate it well enough. Of course lambda calculus is very useful and has plenty of applications, never meant to say otherwise!