5 ms·

What Exactly Are You Trying To Prove?

6 points by hhm 19y ago

fauigerzigerk 19y ago
He's right for most situations, but some things cannot be tested. Concurrency comes to mind. If I'm told that a particular deadlock or inconsistency cannot occur, I prefer formal proof to a green light bulb on 100 test runs. The issue might only crop up at test run 9999999 using a particular cluster of particular CPUs.
- boucher 19y ago
  I too would want a proof, but its wrong to think that you can't test this. It might be difficult, but you absolutely can. Tracking down the order of things that causes the problem is where the troubles comes -- reproducing that order is easy using semaphores or something similar. Of course, for any moderately complex set of interactions, you won't be able to write tests to cover every possibility, which is exactly the point of the main detractor in this article.
  - fauigerzigerk 19y ago
    Sure you could simulate one particular order of things, but if you do that you no longer need tests because you're close to a proof anyway. Tracking down the order of things that causes a problem is debugging, not testing, in my view.
boucher 19y ago
I think the author is pretty off base. I don't mean to say that testing isn't valuable, just yesterday I wrote some unit tests to help me work through a very specific problem. But the assumptions are flawed. The main point of the author is that proving correctness is too difficult. But the same can be said of testing in general. If unit testing is designed to be applied only to the smallest of units, where testing should be obvious, I would argue that an informal correctness proof would be only trivially harder. Take for example the function I often see as the starting point of test driven design presentations: fahrenheitToCelsius() or fToC() Somebody writes the test assertTrue(fToC(32)==0). Alright, well that fails. So I go ahead and write the function: fToC(f) { return 0; } Test passes now. So we write a new test: assertTrue(fToC(-40)==-40). Repeat: fToC(f) { if(f==-40) return -40; return 0;} Maybe that's enough special casing to get someone to finally write (in this presentation): fToC(f) { return (5/9)*(f - 32); } Congratulations, our tests pass. But the presentation points out that fundamentally you start off with the assumption that passing tests is your goal, as opposed to writing verifiably correct code. Proving that this function is correct is trivial, so just write it in the first place. Obviously this is an incredibly contrived example, and perhaps the presentations I have seen on TDD have not been that great, but I think it accurately describes what I see as the main problem with TDD. Tests should be there to idiot proof your code, so that once you've verified your algorithm is correct, and that your code matches that algorithm, the test sits there to decrease the likelihood of a regression through some silly or unrelated change. But to start from the assumption that you will write all the correct tests and thus your code will be verified seems highly suspicious to me.
- fauigerzigerk 19y ago
  I agree with you about the TDD presentations. They usually show exactly the trivial cases that could just as well be proved. But at the end of the day the question is which camp has empirical proof of being able to improve software quality in real world projects. My feeling is that the "correctness proof" camp doesn't have much to show in terms of progress recently. What we're seeing instead is a useless proxy fight between dynamic typing versus static typing proponents about stuff that can just as easily proved as it can be tested.
  - boucher 19y ago
    I agree that this particular argument is pretty pointless, and I even believe that there are plenty of examples of people programming with TDD and having great results. My only problem with the TDD paradigm is that it doesn't work with the way I think about software. It isn't so much about having a formal correctness proof, but when I'm writing code, its incredibly more valuable to me to think it through, reason about the various inputs and outputs, and convince myself that it is a correct solution. And although I usually don't, I see the value in writing tests to verify some of the assumptions you made. I don't, however, see the logic in starting from a set of tests (especially ones that can't possibly know about the specific "pressure points" of the code you will eventually write) and then deriving the solution. But that's just me, and as they say, different strokes...

6 points by hhm 19y ago

He's right for most situations, but some things cannot be tested. Concurrency comes to mind. If I'm told that a particular deadlock or inconsistency cannot occur, I prefer formal proof to a green light bulb on 100 test runs. The issue might only crop up at test run 9999999 using a particular cluster of particular CPUs.

boucher 19y ago
I too would want a proof, but its wrong to think that you can't test this. It might be difficult, but you absolutely can. Tracking down the order of things that causes the problem is where the troubles comes -- reproducing that order is easy using semaphores or something similar. Of course, for any moderately complex set of interactions, you won't be able to write tests to cover every possibility, which is exactly the point of the main detractor in this article.
- fauigerzigerk 19y ago
  Sure you could simulate one particular order of things, but if you do that you no longer need tests because you're close to a proof anyway. Tracking down the order of things that causes a problem is debugging, not testing, in my view.

boucher 19y ago

I think the author is pretty off base. I don't mean to say that testing isn't valuable, just yesterday I wrote some unit tests to help me work through a very specific problem. But the assumptions are flawed. The main point of the author is that proving correctness is too difficult. But the same can be said of testing in general. If unit testing is designed to be applied only to the smallest of units, where testing should be obvious, I would argue that an informal correctness proof would be only trivially harder. Take for example the function I often see as the starting point of test driven design presentations: fahrenheitToCelsius() or fToC() Somebody writes the test assertTrue(fToC(32)==0). Alright, well that fails. So I go ahead and write the function: fToC(f) { return 0; } Test passes now. So we write a new test: assertTrue(fToC(-40)==-40). Repeat: fToC(f) { if(f==-40) return -40; return 0;} Maybe that's enough special casing to get someone to finally write (in this presentation): fToC(f) { return (5/9)*(f - 32); } Congratulations, our tests pass. But the presentation points out that fundamentally you start off with the assumption that passing tests is your goal, as opposed to writing verifiably correct code. Proving that this function is correct is trivial, so just write it in the first place. Obviously this is an incredibly contrived example, and perhaps the presentations I have seen on TDD have not been that great, but I think it accurately describes what I see as the main problem with TDD. Tests should be there to idiot proof your code, so that once you've verified your algorithm is correct, and that your code matches that algorithm, the test sits there to decrease the likelihood of a regression through some silly or unrelated change. But to start from the assumption that you will write all the correct tests and thus your code will be verified seems highly suspicious to me.

fauigerzigerk 19y ago
I agree with you about the TDD presentations. They usually show exactly the trivial cases that could just as well be proved. But at the end of the day the question is which camp has empirical proof of being able to improve software quality in real world projects. My feeling is that the "correctness proof" camp doesn't have much to show in terms of progress recently. What we're seeing instead is a useless proxy fight between dynamic typing versus static typing proponents about stuff that can just as easily proved as it can be tested.
- boucher 19y ago
  I agree that this particular argument is pretty pointless, and I even believe that there are plenty of examples of people programming with TDD and having great results. My only problem with the TDD paradigm is that it doesn't work with the way I think about software. It isn't so much about having a formal correctness proof, but when I'm writing code, its incredibly more valuable to me to think it through, reason about the various inputs and outputs, and convince myself that it is a correct solution. And although I usually don't, I see the value in writing tests to verify some of the assumptions you made. I don't, however, see the logic in starting from a set of tests (especially ones that can't possibly know about the specific "pressure points" of the code you will eventually write) and then deriving the solution. But that's just me, and as they say, different strokes...