The point is about only being able properties marked as pure with special syntax, whatever their implementation

If a compiler makes safety guarantees that aren't actually guarantees, like "this function is pure because you made some naive promises you can't keep", it undermines your ability to rely on any of the verification it does.

It's especially bad to do this if you're going to perform optimizations based on those safety guarantees (thankfully, typescript doesn't do that.) You can say 'don't use the pure keyword then' but the fundamental design of JS means that in practice almost no functions can be pure. The runtime has to identify cases on the fly where pure optimizations are actually valid.

Isn’t that the model of TypeScript though? If your code ever brings in data from an outside source, somewhere in it you’re saying, “trust me, it’s typed as X.”

Though now I’m doubting myself because maybe it’s possible to use complex enough assertion functions to really prove that. But even if you don’t, it’s still an incredibly useful language. You’re basically saying, if X is true then the rest of this program should fit together like so.”

Right, the thing is that a lot of typescript's assertions are valid even without complete top to bottom knowledge of the code being executed. Object shapes, for example, are pretty clean to reason about (proxies do complicate this some, but not nearly as bad as they do purity), which means structural typing stuff can just work. It doesn't matter whether property 'x' is a getter or a value as if all you need to know is whether an object has a property named x, and if you need to know the type that also is something you can check without needing to know whether reading the value has side effects. And shapes/types can be verified at runtime as long as state isn't mutated between verification and use.

You're right that in the end once you pull in outside data you're having to make promises that you may not be able to keep - I just think purity is an especially difficult set of promises to keep, and the existence of proxies and getters in JS (along with how they work) makes purity basically impossible, so it's just a footgun waiting to be used. And TS isn't going to optimize your code using it, so it's not really delivering value either.

Proxies and state-mutating getter functions are pretty edge features of JS tbh