I mostly agree. The caveat is that we can still express things like pointer lifetimes and even arrays-with-lengths in English. E.g. libc is full of arrays-wit

I mostly agree. The caveat is that we can still express things like pointer lifetimes and even arrays-with-lengths in English. E.g. libc is full of arrays-with-lengths, implemented as separate params. Don't get me wrong: I think it is great that more powerful languages automate and check those things. But it is also right for ABIs to be two-steps behind so that they don't tie themselves to a single language. And here is the real problem with ABIs and C -- C is a single language. Ages ago C was a decent lingua franca, because C programs translated to machine code in pretty easy to guess ways, and the job of an ABI was just to formalise those guesses. But nowadays we have aggressive optimisers, expansive definitions of undefined behaviour, clever parameter passing conventions, abstract "memory models" defining concurrency rules and all kinds of other stuff that make C something more than just an obvious abstraction of real-world machines.