4 ms·

I think there's this myth that TDD is one of the best ways to write software and if you admit you don't do it, you'll be seen as a cowboy and will look stupid.

I think there's this myth that TDD is one of the best ways to write software and if you admit you don't do it, you'll be seen as a cowboy and will look stupid. I think the truth is TDD has its pros and cons, and the weight of each pro and con is highly dependent on the project you're doing. - The uncomfortable truth for some is that not doing any testing at all can be a perfectly fine trade off and there's plenty of successful projects that do this. - Sometimes the statically checked assertions from a strongly typed language are enough. - Sometimes just integration tests are enough and unit tests aren't likely to catch many bugs. - For others, going all the way to formal verification makes sense. This has several orders of magnitude higher correctness guarantees along with enormous time costs compared to TDD. For example, the Linux kernel doesn't use exhaustive unit tests (as far as I know) let alone TDD, and the seL4 kernel has been formally verified, both having been successful in doing what they set out to do. I notice nobody ever gets looked down on for not going the formal verification route - people need to acknowledge that automated testing takes time and that time could be spent on something else, so you have to weigh up the benefits. Exhaustive tests aren't free especially when you know for your specific project you're unlikely to reap much in the way of benefits long term and you have limited resources. For example, you're probably (depending on the project) not going to benefit from exhaustive tests for an MVP when you're a solo developer, can keep most of the codebase in your head, the impact of live bugs isn't high, the chance of you building on the code later isn't high and you're likely to drastically change the architecture later. Are there any statistics on how many developers use TDD? There's a lot of "no" answers in this thread but obviously that's anecdotal.

Jimpulse 7y ago
Can you give a run down on formal verification?
- seanwilson 7y ago
  So say you were writing a sorting algorithm and with unit tests (perhaps with TDD) you wrote tests like: - sort([]) should produce [] - sort([1]) should produce [1] - sort([1,3,2]) should produce [1,2,3] - sort([1,5,6,2,3,4]) should produce [1,2,3,4,5,6] You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. With formal verification, you can actually test it sorts for all possible lists with a mathematical proof. You write a maths proof that shows a property like the following holds: - For all lists X, the result of sort(X) will be a permutation of X that is sorted. For example, the proof could take the form of proof by induction where every step in the proof is confirmed correct by the machine (see Coq, Isabelle for more info). When you were doing maths at school, you probably had exercises where you tried a few examples to see if an equation you came up with might hold in general and then you would write a proof to showed it worked for all possible cases (e.g. with induction, by case analysis). The former is similar to unit testing and the latter is similar to formal verification. My point was there's a spectrum of how rigorous your tests are. People talk about TDD like it's the holy grail sometimes but it's nowhere close to how rigorous you can be. If you've tried some formal verification though, you'll realise it's far too expensive for most projects. Likewise, TDD doesn't make sense for all projects. You have to pick your tradeoffs e.g. between time to market vs cost vs ease of refactoring later vs how rigorous the testing is.
  - Izkata 7y ago
    > You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. For the curious, something like this has happened before - and was found with formal verification: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...
  - stingraycharles 7y ago
    Isn’t this formal verification more for algorithms than implementations? Eg if I have to use Coq to prove my code works, what use is that for my C application? Porting the code to Coq seems to defeat the point of formal verification, I can much better use some property based testing method.
    - seanwilson 7y ago
      There's lots of options. You can write an implementation in Coq (it has its own functional language you code in), prove it correct in Coq and then "extract" (like transpiling) it to another language like OCaml for executing. There's ways to map C code into Coq to prove it's correct as well. All of this is machine checked. See the sel4 kernel to get more of a feel for it. Property based testing sits somewhere between regular software testing with unit tests and theorem proving on the spectrum. It's much less time intensive to do but much less rigorous. My point isn't that formal verification is better than everything. It has its trade-offs, just like TDD.

Jimpulse 7y ago

Can you give a run down on formal verification?

seanwilson 7y ago
So say you were writing a sorting algorithm and with unit tests (perhaps with TDD) you wrote tests like: - sort([]) should produce [] - sort([1]) should produce [1] - sort([1,3,2]) should produce [1,2,3] - sort([1,5,6,2,3,4]) should produce [1,2,3,4,5,6] You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. With formal verification, you can actually test it sorts for all possible lists with a mathematical proof. You write a maths proof that shows a property like the following holds: - For all lists X, the result of sort(X) will be a permutation of X that is sorted. For example, the proof could take the form of proof by induction where every step in the proof is confirmed correct by the machine (see Coq, Isabelle for more info). When you were doing maths at school, you probably had exercises where you tried a few examples to see if an equation you came up with might hold in general and then you would write a proof to showed it worked for all possible cases (e.g. with induction, by case analysis). The former is similar to unit testing and the latter is similar to formal verification. My point was there's a spectrum of how rigorous your tests are. People talk about TDD like it's the holy grail sometimes but it's nowhere close to how rigorous you can be. If you've tried some formal verification though, you'll realise it's far too expensive for most projects. Likewise, TDD doesn't make sense for all projects. You have to pick your tradeoffs e.g. between time to market vs cost vs ease of refactoring later vs how rigorous the testing is.
- Izkata 7y ago
  > You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly. For the curious, something like this has happened before - and was found with formal verification: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth...
- stingraycharles 7y ago
  Isn’t this formal verification more for algorithms than implementations? Eg if I have to use Coq to prove my code works, what use is that for my C application? Porting the code to Coq seems to defeat the point of formal verification, I can much better use some property based testing method.
  - seanwilson 7y ago
    There's lots of options. You can write an implementation in Coq (it has its own functional language you code in), prove it correct in Coq and then "extract" (like transpiling) it to another language like OCaml for executing. There's ways to map C code into Coq to prove it's correct as well. All of this is machine checked. See the sel4 kernel to get more of a feel for it. Property based testing sits somewhere between regular software testing with unit tests and theorem proving on the spectrum. It's much less time intensive to do but much less rigorous. My point isn't that formal verification is better than everything. It has its trade-offs, just like TDD.