[lmm]

> What percentage of coders do programming on a turing tape? Is this partial evidence that turing tapes are trash? Does that question even make sense?

Yes it is. Turing machine models are very limited, and a programme to let us achieve the things we can do with Turing machines (mainly runtime analysis) with a better model (i.e. a lambda-calculus style model) is a very good idea.

> The thing is, almost all of pure math is itself is a bridge between different areas of math. Some of these areas are bridged by category theory, some are bridged by other kinds of math, which have less catchy names.

I'd be equally interested in a programme of doing metamathematics in some non-category-theoretic model that was still "normal" mathematics in the same way that category theory is (and ZFC isn't). But I'm not aware of any such competing effort.

[boyobo]

> What percentage of coders do programming on a turing tape? Is this partial evidence that turing tapes are trash? Does that question even make sense? Yes it is. Turing machine models are very limited, and a programme to let us achieve the things we can do with Turing machines (mainly runtime analysis) with a better model (i.e. a lambda-calculus style model) is a very good idea.

What you wrote is a different justification for why turing tapes are worse than lambda calculus. It has nothing to do with the number of people programming on turing tapes, which is the argument that I was responding to. I could easily have used 'lambda calculus' instead of 'turing tape' above. Most people do not code in the lambda calculus. They write haskell or javascript or whatever.

It doesn't mean that the lambda calculus is trash. Likewise, most mathematicians don't work directly with ZFC. Doesn't mean ZFC is trash.

> I'd be equally interested in a programme of doing metamathematics in some non-category-theoretic model that was still "normal" mathematics in the same way that category theory is (and ZFC isn't).

My point is that almost all pure math (e.g: linear algebra, topology, differential geometry, category theory, group theory) is already metamathematics. Of course, there is a spectrum of 'meta-ness' but I think this is a continuous spectrum. I do not think there is a well-defined division between 'mathematics' and 'metamathematics'.

For example, can you give an argument for why, say, the irrationality of sqrt(2) is not 'metamath', yet godel's incompleteness theorem is 'metamath'?

[lmm]

> What you wrote is a different justification for why turing tapes are worse than lambda calculus. It has nothing to do with the number of people programming on turing tapes, which is the argument that I was responding to.

It has everything to do with it: the reason for wanting a lambda-calculus-like model is that lambda-calculus-like models are what working programmers actually program in. If programmers actually used languages that looked like turing tapes then turing tapes would be a good model for talking about programming in.

> I could easily have used 'lambda calculus' instead of 'turing tape' above. Most people do not code in the lambda calculus. They write haskell or javascript or whatever.

Haskell has been described as essentially a typed lambda calculus. You're treating this as a binary distinction when it isn't: there's a lot of value in the model that we can do formal program analysis with being close to the models that we like to program in, whether the models are exactly identical is a lot less significant than the degree of similarity. Likewise the problem that "mathematicians don't work in ZFC" isn't just that mathematicians are doing something slightly different day-to-day, it's that it's a very different paradigm from normal mathematics.

> My point is that almost all pure math (e.g: linear algebra, topology, differential geometry, category theory, group theory) is already metamathematics. Of course, there is a spectrum of 'meta-ness' but I think this is a continuous spectrum. I do not think there is a well-defined division between 'mathematics' and 'metamathematics'.

> For example, can you give an argument for why, say, the irrationality of sqrt(2) is not 'metamath', yet godel's incompleteness theorem is 'metamath'?

I'd argue that irrationality of sqrt(2) is applicable outside of a mathematical context - it's a fact about something we're modelling rather than solely a fact about our models ("2" and "sqrt" are of course abstract models, but they can be applied to model a variety of concrete things that we care about, and you can carry over the irrationality of sqrt(2) into at least some of those contexts, where it will translate into something meaningful and useful). Whereas godel's incompleteness theorem is a map for which there is no territory; it's a fact about abstract models that could never correspond to anything that wasn't an abstract model.

But if you want to regard number theory as a subset of metamathematics then I don't mind. When I say I want to be able to do metamathematics, I mean I want to be able to do all metamathematics; in particular I want to be able to talk about proofs in general. You could argue that the irrationality of sqrt(2) is a statement about proofs, but it's certainly not in a context that allows you to reason about general proofs, and number theory does not give you a first-class way to work with proofs in general (of course the Godel encoding exists, but it's extremely tedious and not useful for practical work). Likewise, as far as I know, there's no way to really talk about (general) proofs directly in terms of group theory or linear algebra.