3 ms·

> Types certainly eliminate various kinds of errors, yet studies did not find that they reduce bugs Right, but this is why I asked about structured programming

by jolux 4y ago

> Types certainly eliminate various kinds of errors, yet studies did not find that they reduce bugs Right, but this is why I asked about structured programming. These things are hard to study by their nature. I understand there’s not a consensus on this, but there are a lot of programmers who feel quite strongly that static types reduce bugs. Maybe that’s not good enough for you! But it’s clear that you accept other practices as beneficial on insufficient evidence. Or maybe you don’t — maybe you don’t think writing correct unstructured programs is harder. > most catastrophic crashes in distributed systems occur not because programmers fail to consider certain exceptional situations This is irrelevant though. The question is not whether static types prevent the most common types of bugs, or the most dangerous (it’s clear that memory safety is more important than static types in that regard.) If static types narrow the problem space to situations where you explicitly made the wrong decision, that’s significant. If there are any bugs caused by not handling exceptional conditions (and we both know that there are), then static type systems help reduce those.

pron 4y ago
> These things are hard to study by their nature. Small effects are hard to study by their nature. Big effects are usually easy to spot. > there are a lot of programmers who feel quite strongly that static types reduce bugs There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. > But it’s clear that you accept other practices as beneficial on insufficient evidence It's not about "accept." I myself practice typed programming without asserting the empirical claim that it reduces bugs, that seems not to be true (or at least, the effect does not seem to be big). > The question is not whether static types prevent the most common types of bugs, or the most dangerous So far, we've failed to show that static types reduce bugs, period. You're allowed to like them and promote them, but your feeling towards them does not make a specific empirical claim more or less true.
- jolux 4y ago
  > There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. This is a really poor comparison. How many people who know enough to judge these things believe that? I can understand that you’re rigorous in the empirical claims you accept here, but surely you can see that experienced software developers have somewhat more basis to make claims about type systems than random people do about homeopathy. > or at least, the effect does not seem to be big Fair enough! It’s probably not as big as testing or code review but I do think it exists. You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopathy. > So far, we've failed to show that static types reduce bugs, period. I mean, how could they not? You still haven’t explained this part, except with vague allusions that the problems they catch are not the most common problems. I’ve explained how static types reduce bugs: by eliminating cases where you intend to handle a case and forget to. I’ll specify that I mean a type system with exhaustivity checking or narrowing with control flow (like TS or Kotlin). This is not an empirical argument, it’s a rational argument, and I still legitimately don’t understand what the flaw is. The way I see it, static type systems restrict operations on types to those known to be valid at compile time. In a sound type system and compiler, the resulting program is guaranteed not to make invalid operations on types at runtime. Dynamic programs are fully free to make invalid operations on types at runtime. Some number of bugs are caused by making invalid operations on types at runtime. Where are those bugs in a statically typed program, if they haven’t been eliminated?
  - adgjlsfhk1 4y ago
    The extra bugs in a statically typed program go in the duplicated code that someone copied and changed the type names on because their type system wasn't flexible enough to let different types share the same code. This means that 3 years later when someone fixed a bug in part of the code, the bug remained in the other copy because the person writing the fix didn't know about the copy. For a simple example, consider Arrow.jl vs the C++ implementation of the Arrow format. The Julia implementation is roughly 1/10th the lines of code (with more functionality), so even if there are 5x more bugs per line, the code still has fewer bugs. Static types definitely reduce bugs per line, but they can still increase bugs per functionality.
    - jolux 4y ago
      But there are plenty of static type systems that let different types share the same code, the problem you describe only exists in nominal type systems (like C++) as far as I know. With structural types like in TypeScript or Go you can express this trivially. For that matter you can do this with subtype polymorphism in most cases. In Rust you can do it with trait objects as long as you control either the type or the trait. Probably there’s a way to do it in C++ too.
  - pron 4y ago
    > but surely you can see that experienced software developers have somewhat more basis to make claims about type systems But experienced software developers, more than "random people", should know that if they make a conjecture, it's tested and isn't verified, they should reconsider their conjecture. > You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopathy. There is no evidence for believing this. If you believe the evidence for TS vs JS in particular, then you should also believe the failure to find a more general effect. > I mean, how could they not? That's an interesting question and there are many answers; I've been interested in the complex subject of software correctness for years, and have written a bit about it (https://pron.github.io/ https://pron.github.io/). The more you study software correctness, the more you learn how complicated it is and that there are no easy answers. In particular, you learn that it's not true that more soundness is always a good path toward more correctness. But if you accept your preconceived notions over empirical study, then there's little hope for making actual progress. > Where are those bugs in a statically typed program, if they haven’t been eliminated? I gave you an example of where they are. If you want to go down the path of thinking about the theory of software correctness, start by convincing yourself that for every JavaScript program there is a Haskell program (perhaps living entirely inside an Either monad) that behaves the same way.

by jolux 4y ago

pron 4y ago

> These things are hard to study by their nature. Small effects are hard to study by their nature. Big effects are usually easy to spot. > there are a lot of programmers who feel quite strongly that static types reduce bugs There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. > But it’s clear that you accept other practices as beneficial on insufficient evidence It's not about "accept." I myself practice typed programming without asserting the empirical claim that it reduces bugs, that seems not to be true (or at least, the effect does not seem to be big). > The question is not whether static types prevent the most common types of bugs, or the most dangerous So far, we've failed to show that static types reduce bugs, period. You're allowed to like them and promote them, but your feeling towards them does not make a specific empirical claim more or less true.

jolux 4y ago
> There are a lot of people who feel quite strongly that homeopathy cures all kinds of diseases, but they've failed to demonstrate that. This is a really poor comparison. How many people who know enough to judge these things believe that? I can understand that you’re rigorous in the empirical claims you accept here, but surely you can see that experienced software developers have somewhat more basis to make claims about type systems than random people do about homeopathy. > or at least, the effect does not seem to be big Fair enough! It’s probably not as big as testing or code review but I do think it exists. You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopathy. > So far, we've failed to show that static types reduce bugs, period. I mean, how could they not? You still haven’t explained this part, except with vague allusions that the problems they catch are not the most common problems. I’ve explained how static types reduce bugs: by eliminating cases where you intend to handle a case and forget to. I’ll specify that I mean a type system with exhaustivity checking or narrowing with control flow (like TS or Kotlin). This is not an empirical argument, it’s a rational argument, and I still legitimately don’t understand what the flaw is. The way I see it, static type systems restrict operations on types to those known to be valid at compile time. In a sound type system and compiler, the resulting program is guaranteed not to make invalid operations on types at runtime. Dynamic programs are fully free to make invalid operations on types at runtime. Some number of bugs are caused by making invalid operations on types at runtime. Where are those bugs in a statically typed program, if they haven’t been eliminated?
- adgjlsfhk1 4y ago
  The extra bugs in a statically typed program go in the duplicated code that someone copied and changed the type names on because their type system wasn't flexible enough to let different types share the same code. This means that 3 years later when someone fixed a bug in part of the code, the bug remained in the other copy because the person writing the fix didn't know about the copy. For a simple example, consider Arrow.jl vs the C++ implementation of the Arrow format. The Julia implementation is roughly 1/10th the lines of code (with more functionality), so even if there are 5x more bugs per line, the code still has fewer bugs. Static types definitely reduce bugs per line, but they can still increase bugs per functionality.
  - jolux 4y ago
    But there are plenty of static type systems that let different types share the same code, the problem you describe only exists in nominal type systems (like C++) as far as I know. With structural types like in TypeScript or Go you can express this trivially. For that matter you can do this with subtype polymorphism in most cases. In Rust you can do it with trait objects as long as you control either the type or the trait. Probably there’s a way to do it in C++ too.
- pron 4y ago
  > but surely you can see that experienced software developers have somewhat more basis to make claims about type systems But experienced software developers, more than "random people", should know that if they make a conjecture, it's tested and isn't verified, they should reconsider their conjecture. > You mentioned the TypeScript study, it’s not like there’s no evidence for believing this like there is with homeopathy. There is no evidence for believing this. If you believe the evidence for TS vs JS in particular, then you should also believe the failure to find a more general effect. > I mean, how could they not? That's an interesting question and there are many answers; I've been interested in the complex subject of software correctness for years, and have written a bit about it (https://pron.github.io/ https://pron.github.io/). The more you study software correctness, the more you learn how complicated it is and that there are no easy answers. In particular, you learn that it's not true that more soundness is always a good path toward more correctness. But if you accept your preconceived notions over empirical study, then there's little hope for making actual progress. > Where are those bugs in a statically typed program, if they haven’t been eliminated? I gave you an example of where they are. If you want to go down the path of thinking about the theory of software correctness, start by convincing yourself that for every JavaScript program there is a Haskell program (perhaps living entirely inside an Either monad) that behaves the same way.