[dbmueller]

I was bothered (for lack of a milder word!) by your use of "proved". As far as I understand, the major problem is that "algorithm" is sort of undefined. To actually prove that TMs are universal, you need to set the formal stage, which implies having a formal definition of an algorithm. But this is not really done, and Church-Turing essentially states that any reasonable formalization of algorithm ends up being equivalent. But this is not tautological at all, to me.

> recursive functions alone are not sufficient to describe all computation.

Any function computable with TM is recursive, and vice versa, so they should be, if you understand "computable" as "computable with a TM". I don't see how this "functions as first class" comes into play here, but I'd be interested anyway?

[kd5bjo]

> I don't see how this "functions as first class" comes into play here, but I'd be interested anyway?

Before Church, functions weren’t considered mathematical objects that could be passed as arguments to another function, for instance. I don’t recall the details, but this allows some computations that can’t be described by recursion of fixed functions.

[fnrslvr]

> Before Church, functions weren’t considered mathematical objects that could be passed as arguments to another function, for instance.

This strikes me as profoundly ahistorical. Mathematicians have considered function spaces as families of objects to be operated upon by higher-order functions (themselves considered objects to be operated on, and so on) long before the 1930s. I'm sure some version of this thinking has been part of the "folklore" of mathematics for centuries, but at the very least you have to recognize that the idea of higher-order functions is subsumed by Cantorian set theory in the 19th century.

Edit: if you mean to say that a formalism for higher-order functions was novel in its presence in a computational calculus, your remark makes a little more sense. But a few remarks on that:

* Already in 1933, Herbrand–Gödel μ-recursion had given a model of computation that was equivalent to the lambda calculus. (This could be the "recursion" that the post you're responding to was referencing.) I guess the μ operator could be regarded as a higher-order function, but functions don't really play a first-class role in the μ-calculus.

* It's probably more accurate to say that the lambda calculus was conceived as a logical formalism, of which Church published only a computational fragment when it became apparent that the original calculus was afflicted with the Kleene-Rosser paradox. Higher-order functions (and predicates) had already played a role in formal logic systems for decades prior to this.