The article's summary is fair, but the title is IMO a bit of a click bait, because the problem as described really is that "shoehorning a richer type system atop an Any-typed language is leaky." The Any type leaks through. The principle that a Map from Any to Any is the only data structure of note leaks through.

Trying to make that work for static validation requires dependent typing: the type of the result depends on the term passed in. Or, you could use row types, record types, or any of the other data structures richly typed languages use at their core to be more expressive of intent than just a Map from Any to Any.

The title is really quite an annoying abuse of the term "leaky abstraction".

Honestly I got hung up on understanding why for Typescript the declaration of `keys` shouldn't be:

let keys = (keyof typeof users)[]

Like I get it's a contrived example and maybe I'm missing some nuance to it, but if we're obsessed with type-safety why are we treating a array of strings as an array of keys (which are more like atoms)?

I thought the answer might be we're looking for duck typing-ish behavior, but then the proposed take signature doesn't work either?