TDD is about making evolution explicit
In functional programming, and fervent advocates of strongly typed languages it is common to hear phrases like: “It compiles; ship it!” or “I don’t need to run it, I already know it compiles”, referring to this notion of being able to write code that gets formally verified by the compiler’s type system. They do know that the Curry-Howard equivalence means that: if they can encode the specification of their problem statement clearly enough in their types; then they are effectively turning their compiler into a theorem proover of sorts, that confirms their specification will be met by some set of values, and thus be “true”; for some implied notion of truth +/- proof.
This would seem counter to another position in software development; specifically Test Driven Development. In fact you will see good functional codebases have a test suite that is meant to complement the type system and confirm additional laws (invariants) of their specification with the assistance of property based testing tools like quickcheck or hedgehog. These same people might easily dismiss writing tests first as an unnecessary burden as it will simply hinder the process of constructing the code proper.
I would argue that is a bit short sighted; and offer the title of this post as a mechanism to bridge “correct by construction” with “only write what is required for the tests to pass”. When practicing TDD we are expected to go through cycles of “Red — Green — Refactor” where each new test further constrains the universe of possible programs that can meet the expectations; initially 𝍥will meet your nonexistent requirements; as you discover and refine the program you need, you will log an entry of the evolution of the requirement as an executable piece of code; the first test; and proceed to implement it. In test driven development, you are expected to do this for all requirements, both functional and nonfunctional:
If 6 months into a project has compilation times become a burden; write code that tracks how long compilation is taking and use that to drive the work you are doing. Has a requirement invalidated a previous test? then ensure the previous test fails along with adding a new test documenting the new requirements. Once the time to run the tests are a problem, you can add a test to track that time as you work towards reducing it, by documenting the new and different strategies that will themselves be logged in your test suites.
It might sound radical, impractical, or even an intractable proposition, but when you understand your test suite can effectively be your work log, you can understand where it is the perfect companion to your wonderfully constructed code that compiles and is ready to ship; you have now provided others, including yourself an elegant, and verified (the tests also compile) journal explaining your solution.
