AFAIK, The first evidence of using higher order functions goes back to Schönfinkel's 1924 paper: On the Building Blocks of Mathematical Logic - where he allowed one to pass functions as arguments to other functions.That seems interesting. However, everything that I've been reading about his work (and Curry's by extension) seems to allude to one thing in some form or the other: [higher order functions]...this eliminates the need for bound variables...What I haven't been able to wrap my head around is - what's the big deal? Why did logicians and mathematicians of that time care about this? And do we as theoreticians, care about this today? Why was it groundbreaking to get rid of bound variables and what impact did (or does) it have on computing (theoretically) as we know it?PS: I'm aware of how his work paved way for $\lambda$-calculus and the impact of it on computing and functional programming in general. My question is mostly directed to the time prior to the creation of $\lambda$-calculus and after Schnfinkel's paper. The fact the Curry independently picked up that line of work, which was later known as combinatory logic too alludes to the importance of Schnfinkel's work. 
Why was Schnfinkel's work on eliminating bound variables in logic so crucial?
lo.logic;soft question;ho.history overview;intuition;function
TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't  whether you deal with (higher-order) logics or -calculus. They're so subtle that binding representations form an open research field, with a competition (the POPLmark challenge) some years ago. There are even jokes by people in the field about the complexity of approaches to binding.So, if you care about metamathematics (and most mathematicians don't), you need to deal with binding. But many mathematicians can safely treat the formalization of binding as if it were a foundational problem.Another point is that binding was the only new problem in languages with higher-order functions, because the theory of languages with binding is just algebra (for constants) + binding. Mitchell's Foundations of Programming Languages actually presents things in this order and is rather enlightening.I'm aware of how his work paved way for -calculus and the impact of it on computing and functional programming in general. My question is mostly directed to the time prior to the creation of -calculus and after Schnfinkel's paper.I must be missing something, but this remark seems to make no difference. Binding in higher-order logics and binding in -calculus seem as hard, so as long as people cared about higher-order logics, they had to deal with binding. I'm biased by using Curry-Howard-isomorphism-based theorem provers that implement logic by simply implementing a type theory (where types are formulas and programs are proof terms), so that I just deal with binding once.On the other hand, IIRC, at the time indeed few cared about Schnfinkel's work  partly because of how he (didn't) publish it  the papers were mostly written by colleagues based on the research he did (see here, page 4); Curry then rediscovered the theory independently.Caveat: I'm not an historian, but a PhD student in PL, so mine is a modern (and hopefully accurate) perspective on the topic.EDIT:Why is binding subtle, a bit more concretelyThere are two facets to it  first, implementing it is hard. Secondly, metamathematics is the mathematics of proof manipulation: this manipulation is typically automatic, that is, it's an algorithm  so essentially, you face all the difficulties of implementation, plus making proofs about them. Below I give examples. The examples have a modern perspective  they are about actually formalized proofs. However, some of the difficulties would extend to accurate manual proofs  as long as you don't cheat on details.This shows that Schnfinkel simply gave the first solution to this problem, but this was far from definitive.Implementing it is subtle because of shadowingThe basic problem in implementation is shadowing. Usually one doesn't reuse the same name for different bound variables. But you can't avoid it in lambda calculus, at least because  functions (and their bound variables) are duplicated: $(\lambda f. f~1 + f~2) (\lambda x . x)$ reduces to $(\lambda x . x)~1 + (\lambda x . x)~2$. This isn't a problem yet, but starting from $(\lambda f x. f (f x))\ (\lambda g y . g~y)\ z$ gives you $(\lambda g y . g~y)\ (\lambda g y . g~y)\ z$ and then $(\lambda y . (\lambda g y . g~y)~y)\ \ z$: now you need to deal with shadowing. You can avoid this, at the cost of complicating the beta-reduction rule.Once you have different variables with the same name, you also need to prevent capture. The simplest example of capture is that applying the function $\lambda x y. x$ (return first argument) to $y$ must not give $\lambda y. y$ (the identity function), but $\lambda y'. y$ (a constant function).What's worse is that the counterexamples to naive algorithms are hard to construct when you know the problem already, let alone when you don't. Bugs in almost correct algorithms often lie undetected for years. I hear that even good students typically fail to come up  (on their own) with the correct definition of capture-avoiding substitution. In fact, PhD students (me included) and professors aren't exempt from these problem.That's one reason why some (including one of the best textbooks on programming languages, Types and Programming Languages by Benjamin Pierce) recommend nameless representation (not quite combinatory logic, even though it has been used, but rather deBrujin indexes).Proofs about it are subtleIt turns out that proofs about binding are no simpler than the implementation, as mentioned above. Of course, correct algorithms exist, and proof about them exist  but without advanced machinery, for each language using binding you need to repeat the proofs, and those proofs are simply very big and annoying if you use the definitions for binding on pen and paper.To exemplify algorithms involved in metamathematics, consider the deduction theorem in logics, that allows composing a proof of $B$ assuming $A$ and a proof of $A$ to get a proof of $B$. To prove that theorem, you actually exhibit an algorithm that works on the syntax of the two proofs involved and produces the syntax for a proof of $B$. This algorithm needs to deal with binding.Next, I looked up my best example of what goes wrong if you try formalizing the standard definition. Russell OConnor (who's on this site) formalized the first Gdel's incompleteness theorem in Coq (a theorem prover of the kind mentioned above)  and that theorem involves a logic (with all the relevant algorithms) in another logic (with the syntax of the first logic coded as numbers). He used the definitions which are used on paper and formalized them directly.Search for substitution or variable and count how often they appear in reference to problems to get an impression.http://r6.ca/Goedel/goedel1.htmlI never use those definitions in my work, but each alternative approach has some downside.