7 ms·

> The dynamic world lets us have inconsistent code that partially works This is precisely why I have nightmares about refactoring dynamic codebases.

Touche 10y ago
If it's tested, you shouldn't.
- willtim 10y ago
  Testing shows the presence, not the absence of bugs. Dijkstra (1969).
  - lucisferre 10y ago
    Same can be said of static type checking so what is your point? Are you suggesting that those working in static languages don't need to write tests? Static type checking generally represents an even lower form of error detection than functional and unit testing does. Sure, it can be convenient to have it, but lately I see a lot of static language novices around here talking about their recent and limited experience with type checking as if they are suddenly experts in the tradeoffs between static and dynamic languages.
    - pka 10y ago
      But, as you surely know, types prove something about a piece of code. This means they can very well prove the absence of (certain) bugs. So generally, the more invariants you manage to capture in your types, the more categories of bugs you can statically prove will never happen.
      - jw- 10y ago
        This is all true, but is it not a problem that most static languages don't let you (easily) specify the kind of invariants people include in unit-tests.
        acjohnson55 10y ago
        Sure. But you write unit tests for those.
    - willtim 10y ago
      > Same can be said of static type checking so what is your point? That isn't true. Static typing offers machine checked proofs of the absence of a whole class of trivial errors; and potentially any invariants you've managed to teach it. My point was that testing does not negate the need for static types, as implied by the previous poster.
      - kazinator 10y ago
        Although "class" sounds big, in fact there is only a countable number of places (nodes in the program's tree) where you can have a type error. The space in which any error whatsoever can occur is astronomical.
        TheDong 10y ago
        Let me give an analogy: Claim: "Getting vaccinated stops a whole class of diseases which might kill you" Your rebuttal: Although "class" sounds big, in fact there are only a countable number of viruses that vaccines save you from. The number of ways in which you can die is astronomical. In the above analogy, as in your original statement, you're completely missing the point that the class of errors / class of diseases is an important class and easily preventable, therefore you should do it. In fact, I think what you've said is the reverse of true. Static typing means that there's a chance of an error at each node in the program's tree because a statically typed and statically compiled language ensures that the program can be rendered as an AST before you ship it to your user. A dynamically typed interpreted language can have an error at literally any character in the entire thing, and you don't have "compile-time" to tell you it's not an error. The class of errors that you're saving yourself from is "every single character of this program could be wrong in a way that results in it not even being representable as an AST; there are astronomically many ways that can occur". In addition, it now goes wrong much later. You have to ensure that you've hit every path with testing before you can be even somewhat confident it's valid code, let alone logically correct and bug-free in other ways. A compiled statically-typed language you waste no more time than a compile-cycle to get that minimal assurance.
        10y ago
    - jdmichal 10y ago
      > Are you suggesting that those working in static languages don't need to write tests? You certainly don't need to write tests that Math.floor will return NaN when you pass it something that's not a number...
      - kazinator 10y ago
        What? NaN is actually a number in the sense of being in the domain of the floating-point type. You seem to be mixing up "not a number" (as in character string or list) versus "not a number" as in a special IEEE representation that has special uses in numeric code. A floor function that returns NaN when given a string, instead of throwing a type mismatch exception, is crap design, and a strawman example of that type of checking. It's not an appropriate use of NaN!
        jdmichal 10y ago
        I agree with you [0], but that's what JavaScript gives us to work with. [0] https://news.ycombinator.com/item?id=11898046 https://news.ycombinator.com/item?id=11898046
  - deleted 10y ago
    [deleted]
- bunderbunder 10y ago
  Unit tests are essential, but they only cover the errors that the person writing the tests thought to write. Given that even the highest coverage code I've ever worked on could still be riddled with bugs, I submit that us humans can be pretty bad at thinking of all the tests we should write. Static typing, by contrast, covers all type errors, which can take care of quite a bit if you know how to use the type system to your advantage. On top of that, if you don't rely on a refactoring tool (which I recommend avoiding for anything non-trivial) then the compiler will guide you to all the spots where that type is being used, which gives you an opportunity to re-evaluate the correctness of the code that uses it. Is it more work? Yes. Is that a bad thing? Many would argue it's a good thing.
  - Touche 10y ago
    I get the benefit of static typing, my above comment was directed at the suggestion that refactoring dynamic code is something to be afraid of. You commonly hear this from people who primarily use static languages. I personally don't feel that the benefits outweigh the cost; namely that I have to babysit a compiler and stop development while I fix compiler errors that are irrelevant to the thing I'm working (if I'm working on widget A and I broke widget B by changing a type, I don't want to fix widget B right now).
    - bunderbunder 10y ago
      There might be another cultural difference there: I've never worked in a place that used a dynamic language for the majority of the code base, but from what you're saying it sounds like simultaneously refactoring and adding features is something you'd consider to be a normal task. I'm used to that being considered a big no-no, because it makes code reviews and source control history harder to understand.
      - kazinator 10y ago
        You can can work on several things at once in your local repo and use "git commit --patch" to separate changes. Of course you never want unrelated changes (different "topics") in the same commit. If a feature is better implemented after a certain refactoring, then you can do that at the same time locally but still separate it out into different commits.
- gertef 10y ago
  When my typechecker writes most of my tests for me, I have time to write features.
  - Touche 10y ago
    If so, I'd say you were writing the wrong kinds of tests before. I work in JavaScript and almost never write type verification tests.
    - zeckalpha 10y ago
      Types in JavaScript aren't very expressive. When you encode your business logic in the type system, even business logic can be "tested" via the type checker.
- mkehrt 10y ago
  Luckily, my compiler writes large piles of tests for me. I call it the typechecker.
  - kazinator 10y ago
    These tests only cover the type space, which is trivial. And doesn't vary at run time. Even under dynamic typing, it's by large immutable: short of special tricks like change-class in Common Lisp, objects are immutable, and most data flow paths carry the same types all the time. For instance, consider a function which calculates the GCD of two integers. Everything in that function is an integer. Your compiler tests it for you: nope, no strings or floats in there: nothing but integers, check! It's basically one test, and it has nothing to do with whether that function calculates the GCD correctly. It will pass even if that function calculates the LCM due to misunderstood requirements.
    - pka 10y ago
      There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d. [0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.agda http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
      - willtim 10y ago
        This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.
      - kazinator 10y ago
        For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.
        pka 10y ago
        For all I know Agreed.
    - 10y ago

Touche 10y ago

If it's tested, you shouldn't.

willtim 10y ago
Testing shows the presence, not the absence of bugs. Dijkstra (1969).
- lucisferre 10y ago
  Same can be said of static type checking so what is your point? Are you suggesting that those working in static languages don't need to write tests? Static type checking generally represents an even lower form of error detection than functional and unit testing does. Sure, it can be convenient to have it, but lately I see a lot of static language novices around here talking about their recent and limited experience with type checking as if they are suddenly experts in the tradeoffs between static and dynamic languages.
  - pka 10y ago
    But, as you surely know, types prove something about a piece of code. This means they can very well prove the absence of (certain) bugs. So generally, the more invariants you manage to capture in your types, the more categories of bugs you can statically prove will never happen.
    - jw- 10y ago
      This is all true, but is it not a problem that most static languages don't let you (easily) specify the kind of invariants people include in unit-tests.
      - acjohnson55 10y ago
        Sure. But you write unit tests for those.
  - willtim 10y ago
    > Same can be said of static type checking so what is your point? That isn't true. Static typing offers machine checked proofs of the absence of a whole class of trivial errors; and potentially any invariants you've managed to teach it. My point was that testing does not negate the need for static types, as implied by the previous poster.
    - kazinator 10y ago
      Although "class" sounds big, in fact there is only a countable number of places (nodes in the program's tree) where you can have a type error. The space in which any error whatsoever can occur is astronomical.
      - TheDong 10y ago
        Let me give an analogy: Claim: "Getting vaccinated stops a whole class of diseases which might kill you" Your rebuttal: Although "class" sounds big, in fact there are only a countable number of viruses that vaccines save you from. The number of ways in which you can die is astronomical. In the above analogy, as in your original statement, you're completely missing the point that the class of errors / class of diseases is an important class and easily preventable, therefore you should do it. In fact, I think what you've said is the reverse of true. Static typing means that there's a chance of an error at each node in the program's tree because a statically typed and statically compiled language ensures that the program can be rendered as an AST before you ship it to your user. A dynamically typed interpreted language can have an error at literally any character in the entire thing, and you don't have "compile-time" to tell you it's not an error. The class of errors that you're saving yourself from is "every single character of this program could be wrong in a way that results in it not even being representable as an AST; there are astronomically many ways that can occur". In addition, it now goes wrong much later. You have to ensure that you've hit every path with testing before you can be even somewhat confident it's valid code, let alone logically correct and bug-free in other ways. A compiled statically-typed language you waste no more time than a compile-cycle to get that minimal assurance.
        10y ago
  - jdmichal 10y ago
    > Are you suggesting that those working in static languages don't need to write tests? You certainly don't need to write tests that Math.floor will return NaN when you pass it something that's not a number...
    - kazinator 10y ago
      What? NaN is actually a number in the sense of being in the domain of the floating-point type. You seem to be mixing up "not a number" (as in character string or list) versus "not a number" as in a special IEEE representation that has special uses in numeric code. A floor function that returns NaN when given a string, instead of throwing a type mismatch exception, is crap design, and a strawman example of that type of checking. It's not an appropriate use of NaN!
      - jdmichal 10y ago
        I agree with you [0], but that's what JavaScript gives us to work with. [0] https://news.ycombinator.com/item?id=11898046 https://news.ycombinator.com/item?id=11898046
- deleted 10y ago
  [deleted]
bunderbunder 10y ago
Unit tests are essential, but they only cover the errors that the person writing the tests thought to write. Given that even the highest coverage code I've ever worked on could still be riddled with bugs, I submit that us humans can be pretty bad at thinking of all the tests we should write. Static typing, by contrast, covers all type errors, which can take care of quite a bit if you know how to use the type system to your advantage. On top of that, if you don't rely on a refactoring tool (which I recommend avoiding for anything non-trivial) then the compiler will guide you to all the spots where that type is being used, which gives you an opportunity to re-evaluate the correctness of the code that uses it. Is it more work? Yes. Is that a bad thing? Many would argue it's a good thing.
- Touche 10y ago
  I get the benefit of static typing, my above comment was directed at the suggestion that refactoring dynamic code is something to be afraid of. You commonly hear this from people who primarily use static languages. I personally don't feel that the benefits outweigh the cost; namely that I have to babysit a compiler and stop development while I fix compiler errors that are irrelevant to the thing I'm working (if I'm working on widget A and I broke widget B by changing a type, I don't want to fix widget B right now).
  - bunderbunder 10y ago
    There might be another cultural difference there: I've never worked in a place that used a dynamic language for the majority of the code base, but from what you're saying it sounds like simultaneously refactoring and adding features is something you'd consider to be a normal task. I'm used to that being considered a big no-no, because it makes code reviews and source control history harder to understand.
    - kazinator 10y ago
      You can can work on several things at once in your local repo and use "git commit --patch" to separate changes. Of course you never want unrelated changes (different "topics") in the same commit. If a feature is better implemented after a certain refactoring, then you can do that at the same time locally but still separate it out into different commits.
gertef 10y ago
When my typechecker writes most of my tests for me, I have time to write features.
- Touche 10y ago
  If so, I'd say you were writing the wrong kinds of tests before. I work in JavaScript and almost never write type verification tests.
  - zeckalpha 10y ago
    Types in JavaScript aren't very expressive. When you encode your business logic in the type system, even business logic can be "tested" via the type checker.
mkehrt 10y ago
Luckily, my compiler writes large piles of tests for me. I call it the typechecker.
- kazinator 10y ago
  These tests only cover the type space, which is trivial. And doesn't vary at run time. Even under dynamic typing, it's by large immutable: short of special tricks like change-class in Common Lisp, objects are immutable, and most data flow paths carry the same types all the time. For instance, consider a function which calculates the GCD of two integers. Everything in that function is an integer. Your compiler tests it for you: nope, no strings or floats in there: nothing but integers, check! It's basically one test, and it has nothing to do with whether that function calculates the GCD correctly. It will pass even if that function calculates the LCM due to misunderstood requirements.
  - pka 10y ago
    There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d. [0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.agda http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
    - willtim 10y ago
      This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.
    - kazinator 10y ago
      For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.
      - pka 10y ago
        For all I know Agreed.
  - 10y ago