> I think it gives the impression that a static type system is doing more than it is actually doing This statement probably gets to the heart of the issue. A

> I think it gives the impression that a static type system is doing more than it is actually doing This statement probably gets to the heart of the issue. A static type system isn't something that just "does things", nor can we conduct a proper analysis when the dialectic is reduced to "static vs dynamic". The first thing to realize is that there exists a spectrum in how much we encode in our type system. Even in weaker type systems like those of Go or Java, we can make illegal states unrepresentable, encode invariants, create typesafe abstractions, etc. Or we could just treat everything as object and not make any attempt to encode anything at all in the type system. In the former case, the aphorism "if your code compiles, it probably works", is more true than in the latter case. The next thing to realize is that the expressiveness of a type system places a ceiling on what can be usefully encoded in that type system. So in languages like Haskell, it's possible to get closer to the "if your code compiles, it probably works" ideal, than in a language with a weaker type system. But even in Haskell, it's possible to just write everything in IO and not make any attempt to encode your constraints in the type system. So in that sense, a type system is just a tool. If wielded effectively, it lets us offload a lot of work to the compiler in a sort of symbiotic back-and-forth. And some languages give us better static typing tools, to make that symbiosis more effective. But if we're not using simpler type systems to their fullest, we're not likely to be pushing against their limits, making it a lot harder to justify more advanced type systems. So "if your code compiles, it probably works" shouldn't be read as a statement of fact, but as an aspirational goal, one that we can move towards by more effective use of our tools.