"more types mean more tokens" - the long awaited triumph of J is at hand https://code.jsoftware.com/wiki/NuVoc

When the models immediately output machine code, we will also learn, I guess, that Grace Hopper was wrong to interpose a layer of intelligibility between it and the human: 'AI assembly has erased the supposed advantage of languages and compilation'.

But she wasn't wrong, and 'AI coding' is, if anything, showing how right she was. But it is the same with types. The facility of LLMs with Lean already shows this to anyone who knows what Lean is. It is early days.