I use hundreds of millions of tokens a month, and LLMs have completely transformed the way I work. They're also, frankly, pretty mid programmers.

No, it really is C, not R^2. Consider product spaces, for example. C^2 ⊗ C^2 is C^4 = R^8, but R^4 ⊗ R^4 is R^16 - twice as large. So you get a ton of extra degrees of freedom with no physical meaning. You can quotient them out identifying physically equivalent states - but this is just the ordinary construction of the complex numbers as R^2/(x^2 + 1).

> but rather, physics uses C because C models the algebra of the thing physics is describing.

That's what C is: R^2, with extra algebraic structure.

Easily.

It would not be. Independent creation is a complete defense against copyright infringement.

Patents, however, do work this way.

Here's an implementation using GADTs and type-level addition

    data Node (level :: Nat) (a :: Type) where
        Leaf :: a -> Node Zero a
        Interior :: a -> (Node l a, Node l a) -> Node (l + 1) a

The infinite tape part isn't some minor detail, it's the source of all the difficulty. A "finite-tape Turing machine" is just a DFA.

But no one actually works like this. There are varying degrees of "semiformality" and what is and isn't acceptable is ultimately a convention, and varies between subfields - but even the laxest mathematicians are still about as careful as the most rigorous physicists.

Constructivists are only interested in constructive proofs: if you want to claim "forall x in X, P(x) is true" then you need to exhibit a particular element of x for which P holds. As a philosophical stance this isn't super rare but I don't know if I would say it's ever been common. As a field of study it's quite valuable.

Finitists go further and refuse to admit any infinite objects at all. This has always been pretty rare, and it's effectively dead now after the failure of Hilbert's program. It turns out you lose a ton of math this way - even statements that superficially appear to deal only with finite objects - including things as elementary as parts of arithmetic. Nonetheless there are still a few serious finitists.

Ultrafinitists refuse to admit any sufficiently large finite objects. So for instance they deny that exponentiation is always well-defined. This is completely unworkable. It's ultrafringe and always has been.

Wildberger is an ultrafinitist.

The issue isn't that it got overridden, it's that it got overridden with a value of the wrong type. An intermediate type signature with `updatedAt` as a key will produce a type error regardless of the type of the corresponding value.

> I'd be very interested to know what you'd do to change the type system here to catch this.

Like the other commenter said, extensible records. Ideally extensible row types, with records, unions, heterogeneous lists, and so on as interpretations, but that seems very unlikely.

Sure. The usual Java-style variance nonsense is probably the most common source, but I see you're not bothered by that, so the next worst thing is likely object spreading. Here's an anonymized version of something that cropped up in code review earlier this week:

    const incomingValue: { name: string, updatedAt: number } = { name: "foo", updatedAt: 0 }

    const intermediateValueWithPoorlyChosenSignature: { name: string } = incomingValue

    const outgoingValue: { name: string, updatedAt: string } = { updatedAt: new Date().toISOString() , ...intermediateValueWithPoorlyChosenSignature }