> You can never, ever write a static type that enforces anything of substance, because for that to happen you’d need to execute arbitrary code within the compil

> You can never, ever write a static type that enforces anything of substance, because for that to happen you’d need to execute arbitrary code within the compiler (as happens with dependent types, and of course there is the constant fear of undecidable or infinite type checking in that system). Static types are a tool. You can use that tool well, or poorly. There are applications that tool plain doesn't fit. But it is absolutely the case that it can be an important part of enforcing things "of substance" from a very real engineering standpoint (whatever you think of them theoretically). My go-to example from my own experience: I was working on an experimental C project in an environment that demanded minimum latency at low-to-moderate throughput on (expensive) commodity hardware. Our approach was to pin individual threads, dedicated to their task, on individual processors which were otherwise unused. Some functions could only be called on certain threads, usually because some resources could only be accessed from specific threads to avoid locking. Providing an additional argument that labelled the thread let us catch when a change in requirements (which is inevitable when the goal is experimentation) meant logic in the hot path could now be moved somewhere else or what have you. Testing might have turned up race conditions; running them down would likely have been substantial effort. The type system told me "you're calling foo on the wrong thread on line 1234, dummy" and it told me that quickly. None of this is to say we shouldn't be testing - indeed, over the course of the project testing caught a handful of deadlocks the types (at least, those types) couldn't prevent. But the types were invaluable.