4 ms·

As a side note: The TDD-ish alternative to this, which I also use sometimes is just adding a test where you pass in undefined on your optionals, and then iterat

by Zyst 9y ago

As a side note: The TDD-ish alternative to this, which I also use sometimes is just adding a test where you pass in undefined on your optionals, and then iterating until the test stops throwing.

pdpi 9y ago
Unfortunately, “has no obvious bugs” is not quite the same as “obviously has no bugs”. TDD gives you the former, static typing the latter (within what can be represented by the type system, of course)
- kerkeslager 9y ago
  Yes, but "within what can be represented by the type system" is a fairly large caveat. Type systems often can't represent intent. int* increment(int* i, int step) { return i + step; } Is there a bug here? Well, that depends on the intent. Did we really intend to add an int to an int*? Even Haskell's type system can't tell what you intend: increment i = i + 11; Did we really intend to add 11 rather than 1, or is that a typo? A unit test would clarify the intent of both these functions, and catch both bugs fairly reliably (if they aren't the intended behavior). Ultimately I think TDD and types guarantee different things, and both are useful/needed.
  - naasking 9y ago
    You have to be willing to use types to express intent. Types are logical propositions, so you have to encode your proposition as a distinct type. You can actually prove many programs correct by exploiting even Java's poor type system: Proving Programs Correct Using Plain Old Java Types, http://lambda-the-ultimate.org/node/5387 http://lambda-the-ultimate.org/node/5387
    - kerkeslager 9y ago
      Okay, can you say how you would reasonably catch the typo in my second example with types? Obviously you have to be willing to use types to express intent, but even if you're willing, types are limited in what kinds of intent they can express.
      - wtetzner 9y ago
        int* increment(int* i, int step) { return i + step; } I think your example is flawed. The real problem here is that you're allowed to add an int to an int* with +. int* is not be of type int, and should therefore require some sort of cast to make it possible to add an int to it. Either that, or require a different operator/function to add to a pointer, e.g.: int* increment(int* i, int step) { return prt_add(i, step); } Not all type systems are equal, and how the type system interacts with the language is important.
        kerkeslager 9y ago
        That's my first example, not my second. I specifically asked about the second example because it's fairly obvious that C's type system is garbage. To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function? increment x = x + 11; ...noting that this typo is reliably caught by a unit test.
        tome 9y ago
        How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge.
        kerkeslager 9y ago
        > How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) This isn't a trick question. You run the test, and see that it fails. If you write the wrong test or the wrong type AND the wrong implementation, they won't help you, but the point of both types and tests is that you have to make two mistakes for a bug to get into production. It's possible that in your test, I could have made the same error in the implementation of `increment`, but it's a great deal less likely than making that error in just the implementation or just the test. And to be clear, I'm not saying any of this as a "types versus unit tests" thing. I've specifically said that both are useful and needed for reliable software. > The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge. You totally can catch this bug with some type systems (Coq, for example), it's just much easier to catch this bug with a unit test in most languages. I think that your boss would probably disagree with you that this bug is not meaningful if it makes it into production. You don't get to pick and choose which bugs are meaningful because they don't support your views.
    - seanmcdirmid 9y ago
      Type languages, especially static ones, are very inexpressive in the kinds of logical propositions they can express. You can try type hacking (working an inexpressive into more expressive propositions), but the results are often not usable in real systems.
      - naasking 9y ago
        The type language's expressiveness is definitely more limited than the term language, but "very inexpressive" is overstating the case. You end up grouping C, for which your claim is absolutely true, along with Agda for which your claim is not really true. Regardless, even with Java's limited expressiveness you can encode some powerful propsitions, as the paper I linked shows.
        deleted 9y ago
        [deleted]
        seanmcdirmid 9y ago
        It may be that COQ and Agda have expressive type systems, but who is writing programs with them? They are not general purpose. The paper you linked uses Java's type system for a mechanized proof, meaning...you probably don't want to be writing that out by hand.
        naasking 9y ago
        > It may be that COQ and Agda have expressive type systems, but who is writing programs with them? They are not general purpose. I think that's overstating it a little too. You don't have to use the dependent types, at their core, Coq and Agda are still functional languages and you can just stick to algebraic sums and products and still enjoy type inference. Most people aren't using these languages for general purpose programming because a) poor tooling, and b) because they are explicitly marketed as research languages.
        seanmcdirmid 9y ago

by Zyst 9y ago

As a side note: The TDD-ish alternative to this, which I also use sometimes is just adding a test where you pass in undefined on your optionals, and then iterating until the test stops throwing.

pdpi 9y ago

Unfortunately, “has no obvious bugs” is not quite the same as “obviously has no bugs”. TDD gives you the former, static typing the latter (within what can be represented by the type system, of course)

kerkeslager 9y ago
Yes, but "within what can be represented by the type system" is a fairly large caveat. Type systems often can't represent intent. int* increment(int* i, int step) { return i + step; } Is there a bug here? Well, that depends on the intent. Did we really intend to add an int to an int*? Even Haskell's type system can't tell what you intend: increment i = i + 11; Did we really intend to add 11 rather than 1, or is that a typo? A unit test would clarify the intent of both these functions, and catch both bugs fairly reliably (if they aren't the intended behavior). Ultimately I think TDD and types guarantee different things, and both are useful/needed.
- naasking 9y ago
  You have to be willing to use types to express intent. Types are logical propositions, so you have to encode your proposition as a distinct type. You can actually prove many programs correct by exploiting even Java's poor type system: Proving Programs Correct Using Plain Old Java Types, http://lambda-the-ultimate.org/node/5387 http://lambda-the-ultimate.org/node/5387
  - kerkeslager 9y ago
    Okay, can you say how you would reasonably catch the typo in my second example with types? Obviously you have to be willing to use types to express intent, but even if you're willing, types are limited in what kinds of intent they can express.
    - wtetzner 9y ago
      int* increment(int* i, int step) { return i + step; } I think your example is flawed. The real problem here is that you're allowed to add an int to an int* with +. int* is not be of type int, and should therefore require some sort of cast to make it possible to add an int to it. Either that, or require a different operator/function to add to a pointer, e.g.: int* increment(int* i, int step) { return prt_add(i, step); } Not all type systems are equal, and how the type system interacts with the language is important.
      - kerkeslager 9y ago
        That's my first example, not my second. I specifically asked about the second example because it's fairly obvious that C's type system is garbage. To be clear, my question is, how would you reasonably catch the typo with types in the following Haskell function? increment x = x + 11; ...noting that this typo is reliably caught by a unit test.
        tome 9y ago
        How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge.
        kerkeslager 9y ago
        > How do you catch this broken unit test? def test_increment(x): assertEqual(increment(x), x - 1) This isn't a trick question. You run the test, and see that it fails. If you write the wrong test or the wrong type AND the wrong implementation, they won't help you, but the point of both types and tests is that you have to make two mistakes for a bug to get into production. It's possible that in your test, I could have made the same error in the implementation of `increment`, but it's a great deal less likely than making that error in just the implementation or just the test. And to be clear, I'm not saying any of this as a "types versus unit tests" thing. I've specifically said that both are useful and needed for reliable software. > The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge. You totally can catch this bug with some type systems (Coq, for example), it's just much easier to catch this bug with a unit test in most languages. I think that your boss would probably disagree with you that this bug is not meaningful if it makes it into production. You don't get to pick and choose which bugs are meaningful because they don't support your views.
  - seanmcdirmid 9y ago
    Type languages, especially static ones, are very inexpressive in the kinds of logical propositions they can express. You can try type hacking (working an inexpressive into more expressive propositions), but the results are often not usable in real systems.
    - naasking 9y ago
      The type language's expressiveness is definitely more limited than the term language, but "very inexpressive" is overstating the case. You end up grouping C, for which your claim is absolutely true, along with Agda for which your claim is not really true. Regardless, even with Java's limited expressiveness you can encode some powerful propsitions, as the paper I linked shows.
      - deleted 9y ago
        [deleted]
      - seanmcdirmid 9y ago
        It may be that COQ and Agda have expressive type systems, but who is writing programs with them? They are not general purpose. The paper you linked uses Java's type system for a mechanized proof, meaning...you probably don't want to be writing that out by hand.
        naasking 9y ago
        > It may be that COQ and Agda have expressive type systems, but who is writing programs with them? They are not general purpose. I think that's overstating it a little too. You don't have to use the dependent types, at their core, Coq and Agda are still functional languages and you can just stick to algebraic sums and products and still enjoy type inference. Most people aren't using these languages for general purpose programming because a) poor tooling, and b) because they are explicitly marketed as research languages.
        seanmcdirmid 9y ago