nyssos

The relevant paragraph literally starts with "In India", where, yes, it's obviously the case that Hindus are not marginalized.

Be absolutely ruthless with technical debt. Opus is perfectly capable of producing idiomatic code in any mainstream language you please, but will seize on any opportunity to justify writing basically-python instead because that's "consistent" with the "convention". Deprive it of that excuse.

I also work on a large complex rust project (>1M LOC) with extensive use of Claude Code. It is very consistent with my experience. Claude frequently subverts the obvious intent of the system - whether that's expressed in comments or types - in the pursuit of "making the build green", as it so often puts it. It, like many junior engineers, has completely failed to internalize the lesson that type errors are useful information and not a bad thing to make go away as soon as possible. It is remarkably capable, but you cannot trust it to have good taste.

Yes, and? Something can be both scare and inadequate to a given task. FAANG L5s cost a pretty penny but I wouldn't trust a random one to prove a crypto library correct.

Agreed that we're not at saturation, but we don't have a canonical "best" either. For example ChatGPT 5.5 + Codex is, in my experience, vastly superior to Opus 4.7 + Claude Code at sufficiently well-specified Haskell, but equally vastly inferior at correctly inferring my intent. Deepseek may well have its own niche, though I haven't used it enough to guess what it might be.

You're presuming too much about what OP's quality standards are. Can SOTA models outperform the average junior engineer? Yes, obviously. Can they match the best human engineers, if those humans were given all the time and interest in the world? Equally obviously not.

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.

I do this for debugging. Models are extremely vulnerable to framing effects and it's usually easier to spin up a fresh instance than it is to get an existing one to generate new hypotheses.

The C that shows up in quantum mechanics is likely an example of this--it's a case of physics having a a circular symmetry embedded in it (the phase of the wave functions) and everyone getting attached to their favorite way of writing it

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.

Classical logic is the presumed default for mathematics, if someone is working in a different system they will say so explicitly.

Lawyer rates are extremely high variance, and the NYT is not hiring anywhere near the median. White shoe firms break $1000/hr routinely.

I thought a partner at a large law firm might get $ 500k or more per year

Easily.

but my understanding of copyright is that if a person when into a clean room and wrote an new article from scratch, without having read any NYT, that just so happened to be exactly the same as an existing NYT article, it would still be a copyright violation.

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

Patents, however, do work this way.

Life expectancy at birth is irrelevant, people who die in infancy don't consume many resources at all. What matters is the percentage of the population that's of working age, and here Germany is fairly typical for a developed country.

Here's a less galactic version. Suppose you're implementing a binary tree where every leaf has to have the same height - a toy model of a self-balancing search tree.

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

Yet Turing machines are about as far from abstract mathematics as one can get, because you can actually build these things in our physical universe and observe their behavior over time (except for the whole "infinite tape" part)

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.

Imaginary numbers aren't a field, so there's no such thing. Clifford algebras over the complex numbers work fine, but it's usually not what the people talking about "geometric algebra" are doing.

"Geometric algebras" are Clifford algebras over the reals. Differential geometry is probably the field where you're most likely to see mathematicians discuss them, though they also come up in certain (closely related) areas of mathematical physics via spinors.

There's no mathematically natural choice. In physical settings, on the other hand, you almost always want the one induced by the metric.

Sorry, yes, typo.

To an extent. A truly completely formal proof, as in symbol manipulation according to the rules of some formal system, no. It's valid or it isn't.

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.

You're conflating a few things here.

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.

That's just a good practice in the general case: an intermediate type that fully described the data wouldn't have saved you from overwriting it unless you actually looked closely at the type signature.

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.

Do you have an anecdote (just one!) of a case where TypeScript's lack of type system soundness bit you on a real application?

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 }

There's not much connection. Typescript's record types aren't sound, but that's far from its only source of unsoundness, and sound structural typing is perfectly possible.

Because you don't want to have to enumerate every possible combination up front. Mixins are probably the closest OO concept.

Informally, a sound type system is one that never lies to you.

Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.

There are two parts:

- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.

- Progress: A well-typed term can be further evaluated if and only if it is not a value.

What do you gain from an unsound type system?

The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.

In Physics, entropy is a property of a bit of matter, it is not related to the observer or their knowledge. We can measure the enthalpy change of a material sample and work out its entropy without knowing a thing about its structure.

Enthalpy is also dependent on your choice of state variables, which is in turn dictated by which observables you want to make predictions about: whether two microstates are distinguishable, and thus whether the part of the same macrostate, depends on the tools you have for distinguishing them.

Scala, OCaml, and Haskell all have very powerful type systems. OCaml and Haskell even have good ones.

Then again, I believe even mathematicians are fine with ideas of an empty set, or of a one-element set being distinct from the element itself.

Especially mathematicians. Distinguishing stuff and structure is a common theme throughout mathematics.