3 ms·

>> Proofs never actually cover absolutely every possible case and we also can have as reliable software without the hard math whatsoever. This is ridiculous. I

>> Proofs never actually cover absolutely every possible case and we also can have as reliable software without the hard math whatsoever. This is ridiculous. If not being able to prove everything doesn't help, we should get rid of type systems altogether. Programmers are so complacent and ignorant to what their compilers provide them out of the box, they forget how many brilliant people, proofs, and countless hours it took to create those features. >> But going into psychology and thinking about making things easy for humans goes against what is generally accepted in CS research. Well, no. Just because you don't understand or care to learn how much pain and work it took to get rid of seemingly arbitrary restrictions of type systems doesn't mean that it is not considered CS research. You think Rust's region types that literally prevent you from leaking memory without garbage collection came out of a hackathon? Java's generics are a usability improvement, isn't it? Do you have any idea about who designed that? Don't even get me started on any of the features in pure languages. And even if you were so blind to reject all of these as improvements, psychology and usability of programming languages is an actual CS research field with its dedicated conferences. Here's a master's course [0] from University of Cambridge Computer Laboratory. [0] https://www.cl.cam.ac.uk/teaching/1011/R201/ https://www.cl.cam.ac.uk/teaching/1011/R201/

zzzcpan 10y ago
I don't see a point in your comment, apart from an emotional "people worked hard" stuff. What's your point? Remember the last couple of bug studies? They didn't show type systems having an effect on reducing number of bugs, but instead showed only significant correlation being number of LOCs. And yet dynamically typed languages require fewer lines to express the same thing.
- throwaway729 10y ago
  > I don't see a point in your comment The point of mathetic's comment was to point out that a lot of ("computer science") mathematics goes into the design of the compilers and interpreters that software engineers use every day. And that it's rather ignorant for a user of one of these modern interpreters or compilers (even of a dynamically typed language!) to claim that this math doesn't matter or isn't useful. > Remember the last couple of bug studies? Which studies? There have been at least half a dozen high profile empirical studies about type systems in top tier conferences in the last 5 or 6 years, and probably dozens more in journals/conferences I don't follow. The empirical evidence is predictably mixed. E.g. Hanenberg has published papers cutting in both directions re: usefulness of type systems. Also, there's still very little empirical evidence about many type systems. There's a lot of Java vs. X comparison papers, but very few rigorous empirical studies on Haskell or SML or OCaml or Scala, for example. And I'm not aware of a single empirical comparative study on a dependently typed language. > They didn't show type systems having an effect on reducing number of bugs Actually, there are empirical studies that show type systems reduce bugs. Also, as a separate matter, your summation of the available evidence is inaccurate to the point of absurdity. There is not a single shred of empirical evidence for your unconditional claim that type systems don't have an effect on reducing bugs. That hypothesis has never experimentally tested. Furthermore, the empirical data we have suggests that hypothesis is wrong. Science works by looking at all the evidence and coming to informed conclusions. Cherry picking the N out of M studies that confirm your priors and then generalizing their results far beyond the parameters of the actual study is the opposite of scientific thought. > but instead showed only significant correlation being number of LOCs.. And yet dynamically typed languages require fewer lines to express the same thing. My OCaml programs are very often far shorter than my Python programs. Again, your unconditioned claims are getting you in trouble. You probably mean to say something like "Java programs are usually longer than Python programs", in which case you have a reasonable critique of Java's type system, but not of type systems in general -- or even of the half dozen type systems that are radically different from Java's and in wide-spread use in production environments. And in fact, most adamant supports of type systems are probably some of the most ardent critics of Java's type system, so rejections of type systems on the basis of Java comparisons are a bit of a straw man IMO. If there's a single thing that ALL of the various empirical PL design researchers could agree on, it's that the sort of unconditioned claims that are made in your post should be avoided.
- mathetic 10y ago
  You see that's what I mean. You have zero understanding of what you're talking about. You think dynamically typed languages came out of thin air? Do you know the difference between a segmentation fault and a dynamic type error?

zzzcpan 10y ago

I don't see a point in your comment, apart from an emotional "people worked hard" stuff. What's your point? Remember the last couple of bug studies? They didn't show type systems having an effect on reducing number of bugs, but instead showed only significant correlation being number of LOCs. And yet dynamically typed languages require fewer lines to express the same thing.

throwaway729 10y ago
> I don't see a point in your comment The point of mathetic's comment was to point out that a lot of ("computer science") mathematics goes into the design of the compilers and interpreters that software engineers use every day. And that it's rather ignorant for a user of one of these modern interpreters or compilers (even of a dynamically typed language!) to claim that this math doesn't matter or isn't useful. > Remember the last couple of bug studies? Which studies? There have been at least half a dozen high profile empirical studies about type systems in top tier conferences in the last 5 or 6 years, and probably dozens more in journals/conferences I don't follow. The empirical evidence is predictably mixed. E.g. Hanenberg has published papers cutting in both directions re: usefulness of type systems. Also, there's still very little empirical evidence about many type systems. There's a lot of Java vs. X comparison papers, but very few rigorous empirical studies on Haskell or SML or OCaml or Scala, for example. And I'm not aware of a single empirical comparative study on a dependently typed language. > They didn't show type systems having an effect on reducing number of bugs Actually, there are empirical studies that show type systems reduce bugs. Also, as a separate matter, your summation of the available evidence is inaccurate to the point of absurdity. There is not a single shred of empirical evidence for your unconditional claim that type systems don't have an effect on reducing bugs. That hypothesis has never experimentally tested. Furthermore, the empirical data we have suggests that hypothesis is wrong. Science works by looking at all the evidence and coming to informed conclusions. Cherry picking the N out of M studies that confirm your priors and then generalizing their results far beyond the parameters of the actual study is the opposite of scientific thought. > but instead showed only significant correlation being number of LOCs.. And yet dynamically typed languages require fewer lines to express the same thing. My OCaml programs are very often far shorter than my Python programs. Again, your unconditioned claims are getting you in trouble. You probably mean to say something like "Java programs are usually longer than Python programs", in which case you have a reasonable critique of Java's type system, but not of type systems in general -- or even of the half dozen type systems that are radically different from Java's and in wide-spread use in production environments. And in fact, most adamant supports of type systems are probably some of the most ardent critics of Java's type system, so rejections of type systems on the basis of Java comparisons are a bit of a straw man IMO. If there's a single thing that ALL of the various empirical PL design researchers could agree on, it's that the sort of unconditioned claims that are made in your post should be avoided.
mathetic 10y ago
You see that's what I mean. You have zero understanding of what you're talking about. You think dynamically typed languages came out of thin air? Do you know the difference between a segmentation fault and a dynamic type error?