2026-03-10

Your Static Types Are Not Safe. Mine Are.

Every software engineer worth their salt has lived through the static vs dynamic debate at least once. It’s a good debate to have, many times even. The arguments are well known but often tackled from different angles. At its core, however, it goes in a similar direction. Static types give confidence, ease of refactoring, guarantees. Dynamic types give flexibility, ease of use and no-fuss development. Both are equally successful at delivering software.

In the end, it’s all about held position, and so - many have it. Some choose static typing. Some choose dynamic. Some sit in the middle. And I have my opinion too. My opinion is that the whole argument is a different argument, and I want to show it.

Java, C#, Go, TypeScript. These are statically typed languages. Java has covariant array holes, C# has the dynamic keyword. Go and TypeScript have any, used often and freely. TypeScript’s type system isn’t sound, and it is not by design - not a freak accident. Documented, intentional, accepted. None of those languages prove correctness. They document intent. They catch the obvious mistakes. I won’t say that it’s pointless. It’s not. It’s useful. Yet not something brought up when discussing how much types matter.

Think about trust. Can a static type system be trusted? Would you trust a system that’s correct 50% of the time? Would you trust a system that’s correct 90% of the time? Is a system wrong 1% of the time trustworthy? Trust in a system is, in the end, a binary thing. You can only trust it when it’s always correct. A lock that locks 99% of the time is not a lock.

Then there are dynamic type systems. Python, Ruby, Clojure, Elixir. There are no static guarantees, and yet they live.

But then, there’s mypy, dialyzer, spec, runtime contracts, REPL-driven development with immediate feedback, mature test-related tooling. And there are many successful production codebases.

In theory the gap is big, but in reality well-disciplined, tool-covered Python is very close to statically typed Java. They both fail the same class of problems. They both catch the same class of mistakes.

The line drawn between them is real. But much thinner than discussions suggest.

And so there’s Go, with nilaway, errcheck, golangci-lint, the mo library. Curated Go that catches nil dereferences, swallowed errors, wrong variants. Mypy on Python catches type mismatches. Dialyzer on Elixir catches, surprisingly, a lot despite its dynamic foundation. Clojure spec enforces data shape at boundaries.

The gap between disciplined dynamic and discipline-less static types might even be negative in some dimensions. Static != safe. Dynamic != reckless.

It’s obvious that tooling impact has its limits. Tooling can enforce convention, but not structure. CI gates are real enforcement, but conventions can be bypassed by engineers in ways compiler guards can’t. Though, with that in mind, is there a difference between a convention covering 99% of cases and a compiler covering 99% of the code?

The ML family.

ML was designed in 1973, around a soundness proof as its central goal. Every sound type system either descends from ML or was built by those who deeply understood the theory. It isn’t accidental correlation. It’s inheritance. Various approaches only rediscovering the same mathematical structure from different viewpoints.

Rust, Haskell, OCaml, F#, Elm. Languages with sound type systems. By design, not accident. All of them have a theoretical foundation - Hindley-Milner, Curry-Howard correspondence, soundness as a theorem - built long before the first line of user code. Exhaustiveness checks. Unrepresentable illegal states. Types as proof, not merely documentation. A system you can trust. That’s the ML family.

Have you heard anyone cite Java as an example when discussing types? Me neither. It’s not that non-MLs are bad languages. Just nobody says “look how safe C# is”.

It’s the same gang over and over. Rust, Haskell, OCaml. Those are the languages brought as arguments. The qualities praised in static typing are always ML-class guarantees. The framing says static vs dynamic, so Java and C# free-ride on a reputation they didn’t earn. And Python takes the blame it didn’t deserve.

Distance from Python to Java can be measured in centimeters. Distance from Java to Rust in parsecs. The whole debate put the dividing line in the wrong place.

Today, the static vs dynamic debate is moot. Tooling, discipline and CI close the practical gap between a well-run dynamic and a poorly-run static system. What isn’t moot - what people are pointing at when praising types - is ML versus the World. This is the real divide. One that has theoretical foundation and measurable consequences.

To gain the upper hand in the debate you need to learn the difference. Or better - learn Haskell. Not to use it, but to understand what a type system that can prove things feels like. So when someone tells you TypeScript makes their codebase safe, you’ll know what safe means to them.

In short: don’t bring a knife to a gunfight. And don’t mistake a knife for a gun just because both are made of metal.

Self-admitted FAQ

Q: Can’t we achieve “synthetic soundness” in Java or Python using advanced tooling?
A: Yes, but that is exactly the point. If both dynamic and static languages require the same external class of tools to reach that level of safety, they are fundamentally similar. It makes them part of “The World” and separates them from the ML family where soundness is intrinsic, not slapped on.
Q: Even a Haskell program will fail if the network goes down or a database crashes. Does soundness even matter?
A: That is a constant. A network failure crashes a Haskell binary, a C# app, and a JavaScript script with equal indifference. External reality doesn’t influence the debate on internal type consistency. True is true for everyone.
Q: Isn’t trust a gradient rather than a binary?
A: If trust isn’t binary, it isn’t trust - it’s just a measurement of quality. Would you trust a bank that only steals from you once a year? No. For trust to exist in a system, it must be absolute. We don’t design for systems that fail 5% of the time; we target 100% success. Everything else is requiring correction.
Q: But ML languages like Rust or Haskell force you to solve “type puzzles” during a simple refactor. Isn’t that a downside?
A: Absolutely. It is a massive tax on flexibility. However, C# and Go don’t have this problem because they aren’t as rigid. They are much closer to JavaScript in that regard. This “soundness tax” is a major consequence that is almost always omitted in the static vs. dynamic debate.
Q: Sound systems can still be buggy, right?
A: Yes, but they cannot be buggy in invisible ways. They prevent an entire class of errors - like bad casts or unhandled edge cases - by requiring you to handle them by default or jump through very obvious hoops to ignore them.
Q: Can’t 100% test coverage achieve the same quality as a sound type system?
A: Maybe, but feedback loops matter. A compiler gives you feedback immediately. A test suite might be sitting at the end of a three-hour CI queue. Given enough time and energy, any spec of dust can become a diamond, but that doesn’t change the nature of the material.
Q: Static types catch some errors, tests catch remaining ones, this is a dynamic differentiator, no?
A: No one ever argues that you write fewer tests for Go than for Python. That argument is only actually true for the ML family. In Rust or Haskell, if the types match, the program generally runs without crashing. For “The World,” the test-harness requirements remain the same regardless of the type system.
Q: Isn’t Rust just too verbose and constrained?
A: It is. Soundness comes with a price. My point is that this gap is never discussed in the “Static vs. Dynamic” debate. People want the benefits of Rust but the “no-fuss” feel of Go. You can’t have both.
Q: But surely C# is “better” than Python?
A: It might be, but that’s not the argument. The argument is that they are much closer to each other than proponents admit. Once you bring tooling into the mix, the gap between C# and Python is measured in centimeters, while the gap to Rust is measured in parsecs.
Q: Does the real world even care about soundness?
A: The real world has its own set of constraints, just like the static vs. dynamic debate. Using “real-world pragmatism” to hand-wave away the lack of soundness is just another way to avoid admitting where the dividing line actually sits.