[pizlonator]

> Wait. This doesn’t make sense to me. Statically typed programming languages cannot be deployed nor can they run with a type error that happens at runtime. Untyped languages CAN run and error out with a type error AT runtime. The inevitable consequence of that truth is this

There is nothing inevitable about the consequence you’re imagining because statically typed languages also reject correct programs.

[threethirtytwo]

It is 100 percent inevitable. Your reasoning here is illogical.

How does a statically typed language rejecting a correct program affect reliability? The two concepts are orthogonal. You’re talking about flexibility of a language but the topic is on reliability.

Let me be clear… as long as a language is Turing complete you can get it to accomplish virtually any task. In a statically typed language you have less ways to accomplish the same task then a dynamically typed language; but both languages can accomplish virtually any task. By logic a dynamically typed language is categorically more flexible than a static one but it is also categorically less reliable.

[foldr]

>How does a statically typed language rejecting a correct program affect reliability?

Because in some cases it will reject code that is simple and obviously correct, which will then need to be replaced by code that is less simple and less obviously correct (but which satisfies the type checker). I don't think this happens most of the time, but it does mean that static typing isn't a strict upgrade in terms of reliability. You are paying for the extra guarantees on the code you can write by giving up lots of correct programs that you could otherwise have written.

[threethirtytwo]

>I don't think this happens most of the time, but it does mean that static typing isn't a strict upgrade in terms of reliability.

It is a strict upgrade in reliability. You're arguing for other benefits here, like readability and simplicity. The metric on topic is reliability and NOT other things like simplicity, expressiveness or readability. Additionally, like you said, it doesn't happen "most" of the time, so even IF we included those metrics in the topic of conversation your argument is not practical.

>You are paying for the extra guarantees on the code you can write by giving up lots of correct programs that you could otherwise have written.

Again the payment is orthogonal to the benefit. The benefit is reliability. The payment is simplicity, flexibility, expressiveness, and readability. For me, personally, (and you as you've seem to indicate) programs actually become more readable and more simple when you add types. Expressiveness and flexibility is actually a foot gun, but that's not an argument I'm making as these are more opinions and therefore unprovable. You're free to feel differently.

My argument is that in the totality of possible errors, statically typed programs have provably LESS errors and thus are definitionally MORE reliable than untyped programs. I am saying that there is ZERO argument here, and that it is mathematical fact. No amount of side stepping out of the bounds of the metric "reliability" will change that.

[bitcompost]

Your definition of reliability seems different to how people use the word. I think most would consider a program that was statically checked, but often produces a wrong result as less reliable than a dynamically checked program that produces the right result.

>My argument is that in the totality of possible errors, statically typed programs have provably LESS errors and thus are definitionally MORE reliable than untyped programs. I am saying that there is ZERO argument here, and that it is mathematical fact. No amount of side stepping out of the bounds of the metric "reliability" will change that.

Making such broad statements about the real world with 100% confidence should already raise some eyebrows. Even through the lens of math and logic, it is unclear how to interpret your argument. Are you claiming that sum of all possible errors in all runnable programs in a statically checked language is less than sum of all possible errors in all runnable programs in an equivalent dynamically checked language? Both of those numbers are infinity, although i remember from school that some infinities are greater than others, I'm not sure how to prove that. And if such statement was true, how does it affect programs written in the real world?

Or is your claim that a randomly picked program from the set of all runnable statically checked programs is expected to have less errors than randomly picked program from the set of all runnable dynamically checked programs? Even this statement doesn't seem trivial, due to correct programs being rejected by type checker.

If your claim is about real world programs being written, you also have to consider that their distribution among the set of all runnable programs is not random. The amount of time, attention span and other resources is often limited. Consider the act of twisting an already correct program in various ways to satisfy the type checker, Consider the time lost that could be invested in further verifying the logic. The result will be much less clear cut, more probabilistic, more situation-dependent etc.

[threethirtytwo]

I think the disagreement here comes from overcomplicating what is actually a very simple claim.

I am not reasoning about infinities, cardinalities of infinite sets, or expectations over randomly sampled programs. None of that is needed. You do not need infinities to see that one set is smaller than another. You only need to show that one set contains everything the other does, plus more.

Forget “all possible programs” and forget randomness entirely. We only need to reason about possible runtime outcomes under identical conditions.

Take a language and hold everything constant except static type checking. Same runtime, same semantics, same memory model, same expressiveness. Now ask a very concrete question: what kinds of failures can occur at runtime?

In the dynamically typed variant, there exist programs that execute and then fail with a runtime type error. In the statically typed variant, those same programs are rejected before execution and therefore never produce that runtime failure. Meanwhile, any program that executes successfully in the statically typed variant also executes successfully in the dynamic one. Nothing new can fail in the static case with respect to type errors.

That is enough. No infinities are involved. No counting is required. If System A allows a category of runtime failure that System B forbids entirely, then the set of possible runtime failure states in B is strictly smaller than in A. This is simple containment logic, not higher math.

The “randomly picked program” framing is a red herring. It turns this into an empirical question about distributions, likelihoods, and developer behavior. But the claim is not about what is likely to happen in practice. It is about what can happen at all, given the language definition. The conclusion follows without measuring anything.

Similarly, arguments about time spent satisfying the type checker or opportunity cost shift the discussion to human workflow. Those may matter for productivity, but they are not properties of the language’s runtime behavior. Once you introduce them, you are no longer evaluating reliability under identical technical conditions.

On the definition of reliability: the specific word is not doing the work here. Once everything except typing is held constant, all other dimensions are equal by assumption. There is literally nothing else left to compare. What remains is exactly one difference: whether a class of runtime failures exists at all. At that point, reliability reduces to failure modes not by preference or definition games, but because there is no other remaining axis. I mean everything is the same! What else can you compare if not the type errors? Then ask the question which one is more reliable? Well… everything is the same except one has run time type errors, while the other doesn’t… which one would you call more “reliable”? The answer is obvious.

So the claim is not that statically typed languages produce correct programs or better engineers. The claim is much narrower and much stronger: holding everything else fixed, static typing removes a class of runtime failures that dynamic typing allows. That statement does not rely on infinities, randomness, or empirical observation. It follows directly from what static typing is.

[foldr]

Readability and simplicity can increase reliability, because simple readable code is easier to review.

[threethirtytwo]

From a practical perspective, most programmers will agree with me when I say that static types are more readable.

[foldr]

Sure. That’s a different kind of argument from the absolutist argument you were making earlier.

[threethirtytwo]

Also Did you read what I wrote? I Covered your argument here DIRECTLY in my response. It's like you read the first sentence and then responded while ignoring the next paragraph.