Thanks, as ever, JB.
I suspect we can even make a stronger claim here. If we accept the notion of program as constructive proof (albeit one with effects–which are deeply confounding compared to the enterprise of mathematics, the theorems of which don’t generate heat when applied, for instance), then refactoring becomes something like a proof that two programs are homotopic (i.e. can be continuously deformed from one into the other).
Analogously, if we think of design as the meta-level work of writing some proof in the first place, then one could reasonably contend that the least interesting results will be the ones we generate without effort; the conjectures are where the action is! From this perspective, there simply is no lofty place from which we can stand, knowing precisely what lemmas (components, perhaps) to write or what existing theorems (say, libraries or services) to rely on.
Finally, as eccentric as some of the most notable mathematicians in history have been, (voluntarily) practicing TDD seems quite innocuous. Even supposing TDD was a purely superstitious ritual, on par with an athlete refusing to change their “lucky socks” during game season, we cannot conclude that the practice isn’t at least valuable to the practitioner.