Test driven development is a craft answer to a seemingly quite formal theoretical problem, verification and validation. This can be seen as a vernacular versus institutional architectural style. We can also compare it to different styles of science. When considering historical astronomy, Roddam Narasimha interprets radically empirical approaches as a different style of science, which he terms “computational positivism”.

[W]hile the Indian astronomer found the epicycle a useful tool of representation, he would cheerfully abandon the classical epicycle if he found something which was more efficient or led to a shorter algorithm and to better agreement with observation. For somebody subscribing to Greek ideals, however, this attitude would presumably seem sacrilegious – the rejection of the epicycle would question the basic assumption that the circle is a perfect figure preferred by nature, and hence precipitate a major philosophical crisis.
—
Narasimha, Axiomatism and Computational Positivism

Or in more familiar terms, the approach of the Keralan School was to discount theories and models and go with whichever calculation was most predictive.

In computing the problem of verification and validation had a clear academic answer. It came from the same school of thought – Dijkstra, Knuth, et al – that delivered major algorithmic and language design innovations, many of which (eg structured programming) were unintuitive conceptual shifts for the working programmer. The answer was formal methods, with the classic citation being Carrol Morgan’s Programming From Specifications. I was trained this way and remain sympathetic, but it hasn’t penetrated everyday practice. (Granted I should read more on the latest work,  but I suspect formal methods suffered from the same misreading of the software crisis as other spec-centric high-modernist schemes. I also suspect they will live again in another form, both good topics for another day.)

Test-driven development, by contrast, saw rapid uptake among working programmers, even if it is short of universal. Formal proof and TDD aren’t equivalent techniques, as one is deductive and one inductive. Proof is also a stronger standard. Both involve some degree of upfront investment, but unit tests are much lower cost to interweave into an existing codebase or introduce in an incremental way. One way to think of TDD is a vernacular style suited to an artisan scale, in contrast with the high cost institutional approach of formal methods. It’s the caravan or service station of refinement from specifications.

This is the hoary old craft-practical vs academic-theoretical dialectic. It’s useful, but obscures as well as reveals. Formal methods practitioners never saw proof as replacing testing, let alone automated testing. On the other side, looking at JUnit as an example, the originators like Kent Beck and Erich Gamma were hardly without university links, and their Smalltalk background wasn’t mainstream. 

This is where Narasimha’s typology seems to apply, the idea of not doing science without theory, but doing science in an alternative mode. One of the striking aspects of TDD as described in the original JUnit essays, like Test Infected, is their relaxed attitude to the ultimate implementation. This is computational positivism – the only measure is whether the formula hits a requisite number of data points. The symbolic coherence of the solution itself is not granted any weight; the code can be spaghetti. Though aesthetically displeasing, there’s an argument that its empirical rigour is more scientifically sound.

The experience of using unit testing widely across a codebase usually shows a different emerging property. By decomposing into testable components, the overall coherence of the design actually tends to improve.

Though Keralan astronomy was superior to European for some hundreds of years, post-Newtownian astronomy finally trumped it for precision, together with a very powerful corresponding theory. The right test for such an ambitious scheme in software would be a computationally positivist one, just as for all the bodgy solutions that preceded it: sure it’s pretty, but does it keep the test bar green?