“Computer science is not about computers”

However, those quotes are not saying "that Turing machines are a more elegant basis for computations, since they are much easier to mathematically reason about." I still consider that statement to be false, and I've substantiated that in my comments.

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.

But that doesn't tell us anything about the usability of the formalism as an actual mechanism for computation, or analysis of computation. In that respect, lambda calculus has proved far more useful, as shown by the examples I mentioned, and many more. Another example is denotational semantics, which maps programming language semantics to lambda calculus.

In fact, one of the inventors of denotational semantics, Dana Scott, developed the first non-trivial model of the lambda calculus, in terms of complete lattices. That model addressed the concreteness issue, albeit decades later, in the early 1970s. It's possible Gödel, Church etc. might still have preferred the Turing tape as an intuition-friendly proof for effective calculability, but it would no longer be possible to reasonably make Gödel's "thoroughly unsatisfactory" claim about the lambda calculus.

Coming back to denotational semantics, I'm pretty sure no-one has ever provided a non-trivial language semantics in terms of a Turing machine - and if you wanted to do that, one of the easiest ways to do it would probably be to implement a compiler from lambda calculus to Turing tape, and generate the Turing representation automatically from that.

More generally, my position could be simply refuted with counterexamples of tractable Turing machine solutions to any of the various problems that lambda calculus has been used to address, like programming language implementations, programming language semantics, duals of logical systems, and proof assistants. To my knowledge, no such examples exist, and the reason for that is because what I'm saying is a fact, not an opinion.

> Myself, I find Conway's game of life to be the superior framework over both lambda calculus and Turing's Logical Computing Machine :-P

I'll agree that the game of life is only slightly less useful than the Turing machine as a model of computation!

My position is that computer science is neither a science nor is it a branch of mathematics.

    ---- Lin Pengcheng

         Creator of Computer Science Management School

         Creator of Management Science Computer School

In the field of management science, my discussion of management principles and warehouse/workshop model is the most scientific, systematic, simple, reliable, clear, and operable.

Whether it is an IT practitioner who takes up a management position, or a manager who becomes an IT industry executive, they can use my theory as a bridge to another kind of science.

The Grand Unified Programming Theory: The Pure Function Pipeline Data Flow with Principle-based Warehouse/Workshop Model

https://github.com/linpengcheng/PurefunctionPipelineDataflow

"Equivalence" has a specific meaning here, though. The term "Turing tarpit" was invented to point out the limits of that equivalence, and any attempts to define computations for Turing machines quickly run into that.

The sense in which I consider Turing machines to be "rather unmathematical" is closely related to this. You can write useful mathematical proofs in lambda calculus - as I've pointed out elsewhere, there are automated proof assistants based on this fact. There's no such equivalent for Turing machines. Theoretically, there could be, due to Turing equivalence, but in practice, no-one wants to exploit that.

Given one formalism that has actively been used for such mathematical purposes, and another that has been actively avoided, I call the latter rather unmathematical by comparison to the former.

People can quibble with my word choice, but it's describing a real, measurable phenomenon, the effects of which have played out predictably over the last 70 years.