On Two Views of Computation in Computer Science

> You're right that some languages simply lack certain capabilities, but that's an issue of access, not computation per se.

Types determine what computations make sense.

> If you're going to go that route, then yeah the CTT is false -- likewise, TMs can't see inside black holes, so they can't "compute" that either.

Careful! I never said the CTT is false. I only said it guarantees nothing about functions whose type is anything other than `nat -> nat` (up to isomorphism).

> But the "computations" referred to in the CTT are assumed to meet certain criteria, e.g. that there's some API exposed for accessing the relevant information (...) Of course you have to care about external state and access privileges and race conditions and whether the API is usable, etc

These are properties of programs, not functions. Two syntactically different programs may compute the same function, so you can't conflate programs with functions (and hope to make sense).

> If you generalize to trees and pick the right alphabet, suddenly every element of your datatype is a well-formed lambda term.

How would you feed trees to the computation? Also, once types are involved, nothing can help you. I admit that untyped LC is somewhat of a borderline case.

> It's also unclear if you're talking about the complexity of type inference or type checking

Doesn't matter in this case. Pick a string representation -- any representation -- and see if it's well-formed. You can include the types and then only type checking would be necessary, or not -- and then it's type inference. Either way, the complexity is significant.

> namely the C abstract machine

That's not a machine model.

> it's undecidable whether a state is meaningful

The same goes for any language and your definition on "meaningful". You can always say that something meaningful is a little finer-grained than the language can express, or the validating the language itself is also undecidable. Got simple types? Only primes are meaningful.

> They just don't have many useful properties compared to more "abstract" approaches, and are mostly used to reason about implementation.

My point is that they're not comparable. A glass of water doesn't have the same useful properties as a blender, yet they're both made of molecules. However, there's an objective difference: a blender consumes far more energy, so of course you can use that energy to do more things.

They do use the word function, just not in terms of the language itself, but in the same sense of saying that a falling apple integrates the function from its mass to acceleration; it's a human interpretation of the encoding. I would state the Church-Turing thesis like so: a universal computation model can compute anything any physical machine can. As Hodges says in one of the links in the article, this is how Church and Turing themselves understood it. How would I define "anything"? As a function on any countable set -- the natural numbers, would do -- and I would explain what it mean to compute a function: pick a function, pick an input element, pick a finite representation for the input and output; if a physical machine can compute the output representation from the input representation, so can a universal computation model.

I could choose a function between any two countable sets, e.g. (Nat -> Nat) -> (Nat -> Nat): pick a representation for the input and output and all models can compute the same functions, and those are the functions that machines can compute. They differ in abilities regarding representation within the model, but as the language models' representation require very significant computational work, I'd expect their representation to do more: they're paying for it.

A C compiler works hard, so you'd expect it to provide you with a representation more suitable to your wishes than machine code. It's just that as a compiler like C translates a "meaningful" language to a machine encoding, everybody notices the work. The language "computation" models work in a vacuum, so I just pointed out that even though they don't translate anything from one representation to another, they still have to pay for their natural representation.

> What actually exists in computing is procedures

You can't free yourself from thinking in terms of languages :) Not a single one of the machine models -- TM, RAM, neural networks, DNA, digital circuits, quantum computers -- has a concept of a procedure. Procedures are language constructs. Whether you choose to compile Pascal or Haskell to x86 machine code is up to you, but in either case there would be a complexity price to pay.

Machine models take bits and they compute bits, period. Like an apple that falls, they just do they're thing. If a person then wants to say, hmm, that apple's path describes an integral of acceleration, or I will assign the input and output bits mathematical objects, and say that the mapping is a function -- they're welcome to do it, but it's not what the computation does.

> A meaningless symbol might as well never have been computed at all.

Everyone agrees on that. But an apple that falls without Newton to grasp its meaning still falls, and a machine still computes. For meaning you have to pay real, measurable complexity. It therefore doesn't make any sense to compare a model that pays that price with one that doesn't.

Academia is feudal and thus no answer to this is about to become widely accepted. :(