Unless your language includes a proper proof system for the entire program logic (see Idris or SPARK/Ada for something close to this, though in the latter it can only work with a subset of the overall Ada language), you will need tests. Even in languages like Haskell, Rust, and Ada which have very good and expressive type systems tests are helpful for validating the actual logic of the system.
Adding larger system tests after the fact is perfectly reasonable. TDD wants you to write tiny tests for every square millimeter of functionality. It's just not worth it, and 99% of the value is to make up for shortcomings in dynamic languages.
Agreed!; Personally, I am of the opinion that Idris for one is mature enough that there is no need to forego tools that have a proper proof system for the entire program. It’s feasible today.
Idris is carefully and purposefully described by its creators as not production ready. Nonetheless, because of what Idris is, it’s arguably more production-ready than languages which don’t even attempt formal soundness to anywhere near the same degree. In other words: Idris is not a complete Idris. But! All the other languages are even less complete Idrises!
Big old “personal opinion” disclaimer here though. –Let’s prove it’s not possible to use Idris by doing it! Shall we?
Yes that’s true, and imho the objective should be to move as much of TDD as possible into the type system. Despite my OP maybe implying it’s binary, it’s not, and getting closer to that objective is just as worthy as getting all the way there. It’s still a hard problem and getting all the way there will take years or decades more experience, experimentation, research, and learning.
Yes, you will need tests, but do you need 1. TDD? 2. Unit tests?
I agree with Jim Coplien when he argues that most unit testing is waste. And TDD is even worse, because it is equivalent to designing a complex system purely from the bottom up, in miniature steps.
> And TDD is even worse, because it is equivalent to designing a complex system purely from the bottom up, in miniature steps. [emphasis added]
What fool uses TDD to design? The second "D" is "Development". If people want to act foolishly, let them. Then come in later and make money cleaning up their mess.
Better design is one of the supposed benefits of TDD. The article nicely demolishes that view, and I agree fully with what it says.
There is a small scale design benefit to writing tests, and that is simply that you always have a "user" of your code, even if it's only focused on tiny bits of it.
But having said that, I get essentially the same design benefit from writing tests afterwards, or writing a test client, or writing user documentation. I usually discover code needs some design improvement once I have to explain or use it.
It leads to better design (is the theory), but it is not itself a design process. It's a development process. TDD doesn't replace the need to stop, think, and consider your design.