4 ms·

> but surely you can see that experienced software developers have somewhat more basis to make claims about type systems But experienced software developers, m

by 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.
- pron 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 don't claim that. Given what we know, the likeliest explanation to the findings so far is that an effect, if it exists, is probably small. > Formal correctness? Bugs per line of code? Both would work. > in which case I think it’s basically a truism that more soundness leads to more correctness. At some cost, perhaps. And you'd be wrong, or, at least, the second part of your statement makes all the difference. What we want is the best correctness we can get for some given cost, or, given some effort, what should you do to get the most correct program? If you follow formal methods, some of the hottest lines of research right now are about reducing soundness to improve correctness. > As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more. I didn't say they did. But you asked how we explain the observation that types don't improve correctness, and one explanation is that the kind of mistakes that types catch aren't the costliest bugs that make it to production, and perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs. > But this is the root of my reasoning. That's as good a conjecture to start with as any, but it needs to be revised with findings.
  - jolux 4y ago
    > perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs I guess in my experience the effort invested programming in a static language is really not that much higher than dynamic, and in some ways I find it less effortful. For example: pattern matching on a sum type, being sure that I’ve handled all the cases I want to. Is there good empirical research on this? > That's as good a conjecture to start with as any, but it needs to be revised with findings. I was attempting to make a factual statement, not a conjecture. If it is true that static types eliminate a class of errors, then type errors must be really cheap for static types not to be worth it on those grounds. My prior is that compiler errors are cheaper than runtime errors here.
    - pron 4y ago
      Until it's been measured, a statement is a conjecture, not "factual." A conjecture that we've tried to verify yet failed to see a large effect is a problematic conjecture. We don't have good empirical findings about many things, most likely because many effects are small at best. But it doesn't matter. You're can say that you still believe something despite failed attempts to measure it, but you can't see it's "factual." That is the difference between fact and conjecture.

by pron 4y ago

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.

pron 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 don't claim that. Given what we know, the likeliest explanation to the findings so far is that an effect, if it exists, is probably small. > Formal correctness? Bugs per line of code? Both would work. > in which case I think it’s basically a truism that more soundness leads to more correctness. At some cost, perhaps. And you'd be wrong, or, at least, the second part of your statement makes all the difference. What we want is the best correctness we can get for some given cost, or, given some effort, what should you do to get the most correct program? If you follow formal methods, some of the hottest lines of research right now are about reducing soundness to improve correctness. > As far as I could tell from reading the study, it’s not evidence that static languages encourage this sort of bug more. I didn't say they did. But you asked how we explain the observation that types don't improve correctness, and one explanation is that the kind of mistakes that types catch aren't the costliest bugs that make it to production, and perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs. > But this is the root of my reasoning. That's as good a conjecture to start with as any, but it needs to be revised with findings.
- jolux 4y ago
  > perhaps the extra effort invested comes at the expense of other approaches that do uncover more serious bugs I guess in my experience the effort invested programming in a static language is really not that much higher than dynamic, and in some ways I find it less effortful. For example: pattern matching on a sum type, being sure that I’ve handled all the cases I want to. Is there good empirical research on this? > That's as good a conjecture to start with as any, but it needs to be revised with findings. I was attempting to make a factual statement, not a conjecture. If it is true that static types eliminate a class of errors, then type errors must be really cheap for static types not to be worth it on those grounds. My prior is that compiler errors are cheaper than runtime errors here.
  - pron 4y ago
    Until it's been measured, a statement is a conjecture, not "factual." A conjecture that we've tried to verify yet failed to see a large effect is a problematic conjecture. We don't have good empirical findings about many things, most likely because many effects are small at best. But it doesn't matter. You're can say that you still believe something despite failed attempts to measure it, but you can't see it's "factual." That is the difference between fact and conjecture.