3 ms·

>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

>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 11y 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 11y 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.
  - knucklesandwich 11y ago
    > No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production. I'm not trying to argue against your experience (or persuade you against it, for that matter). Only making a point that it is possible for you to have type errors that go uncaught by unit tests unless (unless you run those tests against all values). > It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck). Quickcheck takes advantage of types to narrow the inputs for generative tests, whereas dynamic languages have to content with any possible input. >> I believe there is almost no overhead imposed by a static type system > I think that's wishful thinking. Here's a couple ways I think you actually waste more time in dynamic languages: 1. Type checks. Sounds almost tautological, but it's true. Any time you see someone using the type() function in python, you're branching in code for something a compiler could take care of for you. 2. Redundant validation, specifically against a purely functional language that is statically typed. Since types encode facts about data and functions encode theorems, statically typed languages only require one test to verify the assumptions in a theorem. In other words, if there is one function creating values of type Foo with an integer attribute "foo" and it insures that "foo" is 0, I never need to check if foo is 0 anywhere in production code. I only need to check that in a single test of the constructor. In practice I find this means I need to write a lot less tests with a statically typed language, and generally a lot less branches in code. 3. Documentation comprehension. I can't count the number of times I've read a javascript library's documentation only to be thoroughly confused about what kinds of values can be passed to a function legally. Since the language provides no way to enforce this, it seems to encourage a culture of negligence about documenting what invariants of data are required to hold. Furthermore I rarely get a descriptive exception informing me what the issue is, rather I get a type error about a missing attribute or something. 4: Boilerplate code. Fixed data schemas mean you can generate efficiently executing code to perform tasks like serialization, client libraries, etc. Take a look at servant: https://haskell-servant.github.io/ https://haskell-servant.github.io/ Because haskell is statically typed, the type system makes it trivial to generate an HTTP server, a client, and a swagger API docs page all from a couple types. This can be done for certain things in dynamic languages, but since it requires introspection it will almost definitely be slower (and in some cases that may make it impractical to use). 5. Refactoring. Dynamic types are notoriously a pain for editors. Values can be changed ad hoc in ways that make it very difficult to change names without some smart regexes. Refactoring in statically typed languages is a breeze with a sufficiently smart editor/ide. Find and replace is generally two clicks away and is guaranteed to find all occurrences and replace them safely. 6. Condition checking. Pattern matching is not exclusive to statically typed languages, but it is much more common in them. Static type systems also allow for exhaustivity checks that a dynamically typed language cannot perform. In general I think the things people claim are time consuming about statically typed languages are based on older languages that are lacking richer type system features. Things like: 1. Omnipresent type annotations. In haskell you almost never have to specify one of these (in fact you can get near 0% of these if you turn off the monomorphism restriction). The most common use of type annotations in for function signatures, which I find are nice to have for documentation purposes anyways. 2. Inability to perform generalizable code. A lot of people base this on experience with languages like Java, which is unfortunate because the state of the art is much farther ahead. There are many "dynamic feeling" generalizations you can get out of newer statically typed languages. For instance, you can easily generate a "falesy" abstraction similar to python or javascript through haskell typeclasses. Typeclasses, functors, etc. are all examples of statically typed features that allow you to write abstract code over disparate sets of types.
deleted 11y ago
[deleted]
Silhouette 11y ago
>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. Proofs are exactly what the results of strong static type systems give you. They can't prove everything, but they do prove certain things in all possible cases.
- jroesch 11y ago
  If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in understanding, both conceptually, and in modeling your problem. You can also adopt automated verification techniques that can prove strong properties about a system automatically.
  - Silhouette 11y ago
    All true, up to a point at least. Strong, static type systems aren't universal wins with no drawbacks. However, I think it's fair to say that even the "strongish, staticish" type systems in a lot of mainstream languages can still prove very useful properties that are often sources of bugs in the more dynamic languages. A good example would be not accidentally allowing null values to be passed around, as mentioned elsewhere in this discussion. And of course some of less well known but still not uncommon languages, such as the popular functional programming choices or newer offerings like Rust, can do quite a lot more without their type systems becoming an unreasonable burden.
- crdoconnor 11y ago
  >They can't prove everything, but they do prove certain things Much like tests then?
  - mike_hock 11y ago
    Tests actually prove very little. They probe the code with a few, isolated inputs out of a usually very large domain. Their nature is more stochastic. Static type guarantees are actual proofs (barring a compiler bug), and they narrow down the domain that your tests have to probe.

knucklesandwich 11y 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 11y 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.
- knucklesandwich 11y ago
  > No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production. I'm not trying to argue against your experience (or persuade you against it, for that matter). Only making a point that it is possible for you to have type errors that go uncaught by unit tests unless (unless you run those tests against all values). > It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck). Quickcheck takes advantage of types to narrow the inputs for generative tests, whereas dynamic languages have to content with any possible input. >> I believe there is almost no overhead imposed by a static type system > I think that's wishful thinking. Here's a couple ways I think you actually waste more time in dynamic languages: 1. Type checks. Sounds almost tautological, but it's true. Any time you see someone using the type() function in python, you're branching in code for something a compiler could take care of for you. 2. Redundant validation, specifically against a purely functional language that is statically typed. Since types encode facts about data and functions encode theorems, statically typed languages only require one test to verify the assumptions in a theorem. In other words, if there is one function creating values of type Foo with an integer attribute "foo" and it insures that "foo" is 0, I never need to check if foo is 0 anywhere in production code. I only need to check that in a single test of the constructor. In practice I find this means I need to write a lot less tests with a statically typed language, and generally a lot less branches in code. 3. Documentation comprehension. I can't count the number of times I've read a javascript library's documentation only to be thoroughly confused about what kinds of values can be passed to a function legally. Since the language provides no way to enforce this, it seems to encourage a culture of negligence about documenting what invariants of data are required to hold. Furthermore I rarely get a descriptive exception informing me what the issue is, rather I get a type error about a missing attribute or something. 4: Boilerplate code. Fixed data schemas mean you can generate efficiently executing code to perform tasks like serialization, client libraries, etc. Take a look at servant: https://haskell-servant.github.io/ https://haskell-servant.github.io/ Because haskell is statically typed, the type system makes it trivial to generate an HTTP server, a client, and a swagger API docs page all from a couple types. This can be done for certain things in dynamic languages, but since it requires introspection it will almost definitely be slower (and in some cases that may make it impractical to use). 5. Refactoring. Dynamic types are notoriously a pain for editors. Values can be changed ad hoc in ways that make it very difficult to change names without some smart regexes. Refactoring in statically typed languages is a breeze with a sufficiently smart editor/ide. Find and replace is generally two clicks away and is guaranteed to find all occurrences and replace them safely. 6. Condition checking. Pattern matching is not exclusive to statically typed languages, but it is much more common in them. Static type systems also allow for exhaustivity checks that a dynamically typed language cannot perform. In general I think the things people claim are time consuming about statically typed languages are based on older languages that are lacking richer type system features. Things like: 1. Omnipresent type annotations. In haskell you almost never have to specify one of these (in fact you can get near 0% of these if you turn off the monomorphism restriction). The most common use of type annotations in for function signatures, which I find are nice to have for documentation purposes anyways. 2. Inability to perform generalizable code. A lot of people base this on experience with languages like Java, which is unfortunate because the state of the art is much farther ahead. There are many "dynamic feeling" generalizations you can get out of newer statically typed languages. For instance, you can easily generate a "falesy" abstraction similar to python or javascript through haskell typeclasses. Typeclasses, functors, etc. are all examples of statically typed features that allow you to write abstract code over disparate sets of types.

deleted 11y ago

[deleted]

Silhouette 11y ago

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. Proofs are exactly what the results of strong static type systems give you. They can't prove everything, but they do prove certain things in all possible cases.

jroesch 11y ago
If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in understanding, both conceptually, and in modeling your problem. You can also adopt automated verification techniques that can prove strong properties about a system automatically.
- Silhouette 11y ago
  All true, up to a point at least. Strong, static type systems aren't universal wins with no drawbacks. However, I think it's fair to say that even the "strongish, staticish" type systems in a lot of mainstream languages can still prove very useful properties that are often sources of bugs in the more dynamic languages. A good example would be not accidentally allowing null values to be passed around, as mentioned elsewhere in this discussion. And of course some of less well known but still not uncommon languages, such as the popular functional programming choices or newer offerings like Rust, can do quite a lot more without their type systems becoming an unreasonable burden.
crdoconnor 11y ago
>They can't prove everything, but they do prove certain things Much like tests then?
- mike_hock 11y ago
  Tests actually prove very little. They probe the code with a few, isolated inputs out of a usually very large domain. Their nature is more stochastic. Static type guarantees are actual proofs (barring a compiler bug), and they narrow down the domain that your tests have to probe.