6 ms·

> 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

by 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.
- jolux 4y ago
  I don’t think the subject of software correctness in practice is itself well-studied enough to say conclusively that my conjecture is false. I think what can be said conclusively is that at scale people cannot write memory-safe code in an unsafe language or type-safe code in a dynamic language, but obviously these are not the only kinds of correctness. > In particular, you learn that it's not true that more soundness is always a good path toward more correctness. I’m still curious what definition of “correctness” you’re using here. Formal correctness? Bugs per line of code? Generally I’m thinking in terms of formal correctness, in which case I think it’s basically a truism that more soundness leads to more correctness. At some cost, perhaps. > I gave you an example of where they are. Yes, but those bugs are not unique to static languages, and I’ve never claimed that static languages eliminate all kinds of bugs. As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more. To be blunt: I think the set of kinds of bugs that can be written in dynamic languages is a strict superset of the kinds of bugs that can be written in a static language. Maybe I’m completely wrong about this! But this is the root of my reasoning.

by jolux 4y ago

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.

jolux 4y ago
I don’t think the subject of software correctness in practice is itself well-studied enough to say conclusively that my conjecture is false. I think what can be said conclusively is that at scale people cannot write memory-safe code in an unsafe language or type-safe code in a dynamic language, but obviously these are not the only kinds of correctness. > In particular, you learn that it's not true that more soundness is always a good path toward more correctness. I’m still curious what definition of “correctness” you’re using here. Formal correctness? Bugs per line of code? Generally I’m thinking in terms of formal correctness, in which case I think it’s basically a truism that more soundness leads to more correctness. At some cost, perhaps. > I gave you an example of where they are. Yes, but those bugs are not unique to static languages, and I’ve never claimed that static languages eliminate all kinds of bugs. As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more. To be blunt: I think the set of kinds of bugs that can be written in dynamic languages is a strict superset of the kinds of bugs that can be written in a static language. Maybe I’m completely wrong about this! But this is the root of my reasoning.