5 ms·

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. Untyp

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: In the spectrum of runtime errors statically typed languages mathematically and logically HAVE less errors. That by itself is the definition of more reliable. This isn’t even a scientific thing related to falsifiability. This comes from pure mathematical logic. In science nothing can be proven, things can only be falsified. But in math and logic things can be proven and it is provable that static types are more reliable than untyped. It is definitely not vibes and feels. Not all of banking uses statically typed languages but they are as a result living with a less reliable system then the alternative and that is a logical invariant. There are many reasons why someone would choose untyped over typed but reliability is not a reason why they would do this unless they are ignorant.

Spivak 10mo ago
> Statically typed programming languages cannot be deployed nor can they run with a type error that happens at runtime. This is so completely untrue that I'm confused as to why anyone would try to claim it. Type Confusion is an entire class of error and CVE that happens in statically typed languages. Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks. I think the disagreement would come additionally by saying a language like Ruby doesn't actually have any type errors. Like how it can be said that GC languages can't have memory leaks. And that this model is stronger than just compile time checking. Sure you get a thing called TypeError in Ruby but because of the languages dynamism that's not an error the way it would be in C. You can just catch it and move. It doesn't invalidate the program's correctness. Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness.
- akkad33 10mo ago
  > Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks. For this reason Java is a bad example of a typed language. It gives static typing a bad rep because of its inflexible yet unreliable type system (only basic type inference, no ADTs, many things like presence of equality not checked at compile time etc ) Something like ocaml or fsharp have much more sound and capable type systems.
- shepherdjerred 10mo ago
  There are different levels of static typing
- threethirtytwo 10mo ago
  Like other people replying to you C++ and Java gave types a bad rep by being so error prone and having a weak type system. What I am saying is not untrue. It is definitive. Java just has a broken type system and it has warped your view. The article is more talking about type systems from functional programming languages where type errors are literally impossible. You should check out elm. It’s one of the few languages (that is not a toy language and is deployed to production) where the type system is so strong that run time errors are impossible. You cannot crash an elm program because the type system doesn’t allow it. If you used that or Haskell for a while in a non trivial way it will give you deeper insight into why types matter. > Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness. This isn’t safety. Safety is when the program doesn’t even run or compile with a syntax error. Imagine if programs with syntax errors still tried their best effort to run… now you have a program with unknown behavior because who knows what that program did with the syntax error? Did it ignore it? Did it try to correct it? Now imagine that ruby program controlling a plane. That’s not safe.
pizlonator 10mo ago
> 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 10mo ago
  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 10mo ago
    >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 10mo ago
      >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.
thefaux 10mo ago
This logic is both too broad and rigid to be of much practical use[1]. It needs to be tightened to compare languages that are identical except for static type checks, otherwise the statically typed language could admit other kinds of errors (memory errors immediately come to mind) that many dynamic languages do not have and you would need some way of weighing the relative cost to reliability of the different categories of errors. Even if the two languages are identical except for the static types, then it is clearly possible to write programs that do not have any runtime type errors in the dynamic language (I'll leave it as an exercise to the reader to prove this but it is very clearly true) so there exist programs in any dynamic language that are equally reliable to their static counterpart. [1] I also disagree with your definition of reliability but I'm granting it for the sake of discussion.
- threethirtytwo 10mo ago
  You’re objecting on the wrong axis. The claim was about reliability and lack of empirical evidence. Once framed that way, definitions matter. My argument is purely ceteris paribus: take a language, hold everything constant, and add strict static type checking. Once you do that, every other comparison disappears by definition. Same runtime, same semantics, same memory model, same expressiveness. The only remaining difference is the runtime error set. Static typing rejects at compile time a strict subset of programs that would otherwise run and fail with runtime type errors. That is not an empirical claim; it follows directly from the definition of static typing. This is not hypothetical either. TypeScript vs JavaScript, or Python vs Python with a sound type checker, are real examples of exactly this transformation. The error profile is identical except the typed variant admits fewer runtime failures. Pointing out that some dynamic programs have no runtime type errors does not contradict this. It only shows that individual programs can be equally reliable. The asymmetry is at the language level: it is impossible to deploy a program with runtime type errors in a sound statically typed language, while it is always possible in a dynamically typed one. That strictly reduces the space of possible runtime failures. Redefining “reliability” does not change the result. Suppose reliability is expanded to include readability, maintainability, developer skill, team discipline, or development velocity. Those may matter in general, but they are not variables in this comparison. By construction, everything except typing is held constant. There is literally nothing else left to compare. All non-type-related factors are identical by assumption. What remains is exactly one difference: the presence or absence of runtime type errors. At that point, reliability reduces to failure count not as a philosophical choice, but because there is no other dimension remaining. Between two otherwise identical systems, the one that can fail in fewer ways at runtime is more reliable. That conclusion is not empirical, sociological, or debatable. It follows directly from the setup.

Spivak 10mo ago

> Statically typed programming languages cannot be deployed nor can they run with a type error that happens at runtime. This is so completely untrue that I'm confused as to why anyone would try to claim it. Type Confusion is an entire class of error and CVE that happens in statically typed languages. Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks. I think the disagreement would come additionally by saying a language like Ruby doesn't actually have any type errors. Like how it can be said that GC languages can't have memory leaks. And that this model is stronger than just compile time checking. Sure you get a thing called TypeError in Ruby but because of the languages dynamism that's not an error the way it would be in C. You can just catch it and move. It doesn't invalidate the program's correctness. Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness.

akkad33 10mo ago
> Java type shenanigans are endless if you want some fun but baseline you can cast to arbitrary types at runtime and completely bypass all compile time checks. For this reason Java is a bad example of a typed language. It gives static typing a bad rep because of its inflexible yet unreliable type system (only basic type inference, no ADTs, many things like presence of equality not checked at compile time etc ) Something like ocaml or fsharp have much more sound and capable type systems.
shepherdjerred 10mo ago
There are different levels of static typing
threethirtytwo 10mo ago
Like other people replying to you C++ and Java gave types a bad rep by being so error prone and having a weak type system. What I am saying is not untrue. It is definitive. Java just has a broken type system and it has warped your view. The article is more talking about type systems from functional programming languages where type errors are literally impossible. You should check out elm. It’s one of the few languages (that is not a toy language and is deployed to production) where the type system is so strong that run time errors are impossible. You cannot crash an elm program because the type system doesn’t allow it. If you used that or Haskell for a while in a non trivial way it will give you deeper insight into why types matter. > Ruby is so safe in it's execution model that Syntax Errors don't invalidate the running program's soundness. This isn’t safety. Safety is when the program doesn’t even run or compile with a syntax error. Imagine if programs with syntax errors still tried their best effort to run… now you have a program with unknown behavior because who knows what that program did with the syntax error? Did it ignore it? Did it try to correct it? Now imagine that ruby program controlling a plane. That’s not safe.

pizlonator 10mo ago

> 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 10mo ago
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 10mo ago
  >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 10mo ago
    >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.

thefaux 10mo ago

This logic is both too broad and rigid to be of much practical use[1]. It needs to be tightened to compare languages that are identical except for static type checks, otherwise the statically typed language could admit other kinds of errors (memory errors immediately come to mind) that many dynamic languages do not have and you would need some way of weighing the relative cost to reliability of the different categories of errors. Even if the two languages are identical except for the static types, then it is clearly possible to write programs that do not have any runtime type errors in the dynamic language (I'll leave it as an exercise to the reader to prove this but it is very clearly true) so there exist programs in any dynamic language that are equally reliable to their static counterpart. [1] I also disagree with your definition of reliability but I'm granting it for the sake of discussion.

threethirtytwo 10mo ago
You’re objecting on the wrong axis. The claim was about reliability and lack of empirical evidence. Once framed that way, definitions matter. My argument is purely ceteris paribus: take a language, hold everything constant, and add strict static type checking. Once you do that, every other comparison disappears by definition. Same runtime, same semantics, same memory model, same expressiveness. The only remaining difference is the runtime error set. Static typing rejects at compile time a strict subset of programs that would otherwise run and fail with runtime type errors. That is not an empirical claim; it follows directly from the definition of static typing. This is not hypothetical either. TypeScript vs JavaScript, or Python vs Python with a sound type checker, are real examples of exactly this transformation. The error profile is identical except the typed variant admits fewer runtime failures. Pointing out that some dynamic programs have no runtime type errors does not contradict this. It only shows that individual programs can be equally reliable. The asymmetry is at the language level: it is impossible to deploy a program with runtime type errors in a sound statically typed language, while it is always possible in a dynamically typed one. That strictly reduces the space of possible runtime failures. Redefining “reliability” does not change the result. Suppose reliability is expanded to include readability, maintainability, developer skill, team discipline, or development velocity. Those may matter in general, but they are not variables in this comparison. By construction, everything except typing is held constant. There is literally nothing else left to compare. All non-type-related factors are identical by assumption. What remains is exactly one difference: the presence or absence of runtime type errors. At that point, reliability reduces to failure count not as a philosophical choice, but because there is no other dimension remaining. Between two otherwise identical systems, the one that can fail in fewer ways at runtime is more reliable. That conclusion is not empirical, sociological, or debatable. It follows directly from the setup.