People say that "talking about TDD hardly works, if you want to convince someone to TDD, show them results". However, I'm already getting great results without TDD. Showing me that people who use TDD get good results won't be convincing, I want to see that people who write both TDD and not-TDD get better results with TDD.
Despite all of this, I'm interested in giving TDD a try. However I'm not convinced I will gain anything from this. If it does prove useful, I will try to push it to the rest of my team.
My main question is this:
Would TDD serve any purpose for code, if I can already prove the code correctness?
Obviously, neither one is a silver bullet. Your proof might be wrong because you missed a detail, and your test might fail to spot a bug that you failed to test for. In the end, we're human, nobody can make 100% bug-free-code forever. We can only strive to get as close as possible.
However, would TDD actually save any time on code that had its correctness proven? i.e. code that, in the state machine that the code operates on, all valid possible states and their ranges are recognized by the developer, all are accounted for, and the code is designed in a whitelist-style error-checking that passes every exception to an upper handler to make sure nothing unexpected leaks -> without both displaying a (within-reason-)relevant message to the client and sending log notifications to an admin.
Answers with real-life examples would be better.
Some clarifications:
-
This question is not about whether you can prove code correctness or not. Lets assume by default that not all code can be proven correct within a reasonable timeframe, but that some pieces of code can be. For example, it's very easy to proven correctness of a FizzBuzz module. Not very easy for a cloud-based data syncing service.
-
Within this confine, the question asks the following:
Start with the assumption that a codebase is divided into 2 parts: [I] parts that have been proven correct [II] parts that have not been proven correct, but manually tested to work. -
I want to apply TDD practices to this codebase that did not have them until now. The question asks the following: should TDD be applied to every single module, or would it be enough to apply them to only modules that were not proven correct?
-
"Proven correct" means that you can consider this module completely functional-style, i.e., it does not rely on any global or outer state outside itself, and has entirely its own API for I/O that other modules that interact with it must follow. It is not possible to "break this module" by changing code outside the module, at worst you can misuse it and get formatted error messages returned to you.
-
Obviously, every rule has exceptions, compiler bugs in new compiler versions may introduce bugs to this module, but the same bugs could be introduced to tests that tested it and result in a false sense of safety from tests that no longer work as intended. The bottom line is that tests are not a magical solution, they're another layer of protection, and this question discusses the issue of whether this layer of protection is worth the effort in the specific case of a module that was proven correct (assume that it was indeed).
Best Answer
Yes.
Proofs are fine when they're available, but even at the best of times they only prove that a single bit of code will work as expected (for all inputs? accounting for interruptions in the middle of any operation? what about running out of memory? disk failure? network failure?).
What happens when it changes?
Tests are great because they serve as an implied contract about what the code should do. They provide some scaffolding so that your new intern can go in and make changes with some level of confidence. All via quick, clear results: pass or fail.
And frankly, I can coach an intern to write viable unit tests in a few months. I doubt that anyone on my team (myself included) could create proofs that guarantee anything meaningful for non-trivial code; let alone do it quickly and accurately.