22 ms·

Honestly, I feel like the current is going the opposite direction here. In the mid-to-late 2000s the most ascendent languages seemed to be dynamic ones. Ruby, P

Honestly, I feel like the current is going the opposite direction here. In the mid-to-late 2000s the most ascendent languages seemed to be dynamic ones. Ruby, Python, PHP, Javascript, etc. Perhaps that's web solipsism, but those are the languages I remember having the highest visibility from that time. Currently, the tide seems to be changing to towards static typing (and stronger typing). Swift, rust, go, scala, etc. Already statically typed languages seem to be borrowing ideas from their stronger typed brethren. C++ gaining concepts (similar to typeclasses from haskell), Java encouraging the use of Optional (similar to Maybe sum types) for nullable values, etc. Many dynamic languages seem to be providing type checking as an option. Clojure, python with PEP 484, various javascript dialects and type system addons, etc. Tests are important and should supplement a static type system, since there are many classes of bugs a static type system can't prevent. But the benefits of static typing as opposed to TDD for verifying the same thing are obvious to me: 1. Tests are not proofs. Unless a test is exhaustive on the set of inputs accepted, it cannot prove that a piece of code works correctly. Types can prove that certain inputs can never be received by a piece of code, which is a stronger guarantee. 2. Tests are more work. Why write tests to verify assertions that a compiler can prove for me? In practice I find this means that unit tests attempting to verify correct behavior for incorrect inputs have gaps or are imperfect because of lack of time or lack of foresight. 3. Tests are still code. Test assertions can have bugs in the same way that regular code can have bugs. True enough, a type system is also code and can also have bugs, but the code in a type system is more visible and more attended to. In practice, I have found many bugs from flawed test assertions and none from a broken type system (as far as I know).

crdoconnor 10y ago
>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. >Tests are more work I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will usually catch type errors in a dynamically typed language that a statically typed language picks up at compile time. The question is whether you need to write more tests (probably you do...maybe 5% more), and whether the greater number of tests offsets the greater amount of code you need to write to statically type your code. As far as I'm concerned, that's not an easily answered question. >Tests are still code. Test assertions can have bugs in the same way that regular code can have bugs Ditto for types.
- knucklesandwich 10y ago
  > Neither is static typing. It's a layer of protection, much like tests. Not true. The curry-howard correspondence shows the relationship between typed programs and proofs. I recommend you watch a Phillip Wadler talk about this: https://www.youtube.com/watch?v=aeRVdYN6fE8 https://www.youtube.com/watch?v=aeRVdYN6fE8 Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. > I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will catch type errors in a dynamically typed language that a statically typed language picked up at compile time.. This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases). A type system can reject inputs by virtue of their lack of conformance to a type, which eliminates the need to test them. > The question is whether you need to write more tests and whether the greater number of tests offsets the greater amount of code you need to write to statically type your code. I don't have any evidence to support this (if someone does or has proof to the contrary, I'd love to see it referenced here), but I believe there is almost no overhead imposed by a static type system with type inference. > Ditto for types. I acknowledged this above, you just removed that part from the quote. In practice I've never had a bug with the type system (that I'm aware of), while I've seen hundreds of bugs from incorrect test assertions.
  - crdoconnor 10y ago
    >Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. Type systems can verify certain properties about code much like a test does, but that's far from being a mathematical proof of program correctness (especially since compilers have, you know, bugs). >This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases). No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production. It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck). I'd estimate that maybe 5% of errors I experience in production are type related (in a dynamically typed language). That's offset against quicker development time (which also eans ease of fixing the other 95%). >I believe there is almost no overhead imposed by a static type system I think that's wishful thinking. >In practice I've never had a bug with the type system (that I'm aware of) Which type system have you never had a bug with? I've dealt with several buggy, crappy type systems? >In practice I've never had a bug with the type system I've seen plenty of bugs caused by picking the wrong type. >I've seen hundreds of bugs from incorrect test assertions. So have I. Different types of bugs though. The kind which static typing doesn't help eliminate.
smitherfield 10y ago
>Types can prove that certain inputs can never be received by a piece of code, which is a stronger guarantee. I'd amend this to say that sometimes the compiler can prove you're calling a function with or setting a variable to an incorrectly-typed input, but at runtime a strong type system by itself doesn't prevent receiving those inputs, only executing them. It is possible to create a programming language with semantics such that the compiler will always catch incorrectly-typed inputs, but that's a separate but related concept from the type system.
kyllo 10y ago
A countercurrent is the rise of data science, machine learning and statistical programming in industry. Dynamic languages such as R and Python are the tools of that trade, because of the exploratory nature of the programming work that leads to an emphasis on speed and flexibility over correctness, and the loosely typed nature of datasets in the wild.
- SixSigma 10y ago
  Julia has the best of both with the Any type. You can write Dynamic code and then tighten it up when you've got your system worked out.
- knucklesandwich 10y ago
  Good point, though I wouldn't say any of those languages represent new developments (Julia would be a good counterexample though). My understanding is that many of the new probabilistic programming languages are statically typed (hakaru, figaro, BLOG, etc.), though I'm not an expert in this field so I can't speculate on if that represents a coming tide change or not.

crdoconnor 10y ago

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. >Tests are more work I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will usually catch type errors in a dynamically typed language that a statically typed language picks up at compile time. The question is whether you need to write more tests (probably you do...maybe 5% more), and whether the greater number of tests offsets the greater amount of code you need to write to statically type your code. As far as I'm concerned, that's not an easily answered question. >Tests are still code. Test assertions can have bugs in the same way that regular code can have bugs Ditto for types.

knucklesandwich 10y ago
> Neither is static typing. It's a layer of protection, much like tests. Not true. The curry-howard correspondence shows the relationship between typed programs and proofs. I recommend you watch a Phillip Wadler talk about this: https://www.youtube.com/watch?v=aeRVdYN6fE8 https://www.youtube.com/watch?v=aeRVdYN6fE8 Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. > I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will catch type errors in a dynamically typed language that a statically typed language picked up at compile time.. This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases). A type system can reject inputs by virtue of their lack of conformance to a type, which eliminates the need to test them. > The question is whether you need to write more tests and whether the greater number of tests offsets the greater amount of code you need to write to statically type your code. I don't have any evidence to support this (if someone does or has proof to the contrary, I'd love to see it referenced here), but I believe there is almost no overhead imposed by a static type system with type inference. > Ditto for types. I acknowledged this above, you just removed that part from the quote. In practice I've never had a bug with the type system (that I'm aware of), while I've seen hundreds of bugs from incorrect test assertions.
- crdoconnor 10y ago
  >Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. Type systems can verify certain properties about code much like a test does, but that's far from being a mathematical proof of program correctness (especially since compilers have, you know, bugs). >This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases). No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production. It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck). I'd estimate that maybe 5% of errors I experience in production are type related (in a dynamically typed language). That's offset against quicker development time (which also eans ease of fixing the other 95%). >I believe there is almost no overhead imposed by a static type system I think that's wishful thinking. >In practice I've never had a bug with the type system (that I'm aware of) Which type system have you never had a bug with? I've dealt with several buggy, crappy type systems? >In practice I've never had a bug with the type system I've seen plenty of bugs caused by picking the wrong type. >I've seen hundreds of bugs from incorrect test assertions. So have I. Different types of bugs though. The kind which static typing doesn't help eliminate.

smitherfield 10y ago

>Types can prove that certain inputs can never be received by a piece of code, which is a stronger guarantee. I'd amend this to say that sometimes the compiler can prove you're calling a function with or setting a variable to an incorrectly-typed input, but at runtime a strong type system by itself doesn't prevent receiving those inputs, only executing them. It is possible to create a programming language with semantics such that the compiler will always catch incorrectly-typed inputs, but that's a separate but related concept from the type system.

kyllo 10y ago

A countercurrent is the rise of data science, machine learning and statistical programming in industry. Dynamic languages such as R and Python are the tools of that trade, because of the exploratory nature of the programming work that leads to an emphasis on speed and flexibility over correctness, and the loosely typed nature of datasets in the wild.

SixSigma 10y ago
Julia has the best of both with the Any type. You can write Dynamic code and then tighten it up when you've got your system worked out.
knucklesandwich 10y ago
Good point, though I wouldn't say any of those languages represent new developments (Julia would be a good counterexample though). My understanding is that many of the new probabilistic programming languages are statically typed (hakaru, figaro, BLOG, etc.), though I'm not an expert in this field so I can't speculate on if that represents a coming tide change or not.