Your description of TDD is a pretty blatant misrepresentation of the actual philosophy and techniques.
Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check.
Sure, extensive formal verification of all software would probably bring some benefit in terms of correctness and perhaps security. But you're not considering the cost involved.
So far, such verification has only proven to be possible in rather limited situations, namely where there are significant resources available, or in academic exercises. Maybe this will change in the future, but in the present it's generally far more cost-effective to use a statically-typed programming language along with some form of automated testing. That gives many of the benefits of more formal methods of verification, but while also avoiding many of the costs, even if the end result doesn't conform to some theoretical idea of "perfection".
The QuickCheck model is at least as good as unit tests and is more likely to actually find bugs and corner cases. The resulting code is no more complex either. The only drawback I see is that it requires you to design your code in a very modular way that makes things amenable to automated input generation.
Yes, but unit tests and TDD are not synonymous. TDD is a design technique first and a testing tool second. It's goal is to get you to a good design place, not produce a unit test suite - let alone one with 100% coverage.
I love declarative testing tools like QuickCheck. They're excellent. I still test-drive my code though.
Really confused at why this comment is being so harshly downvoted, it seems fairly accurate, possibly downplaying how useful formal verification may be in the future, but the parent is most definitely misrepresenting the practicality and usefulness of TDD
The reality is that programming is an engineering endeavor, and in the face of limited resources, we have to choose the tools that can offer realistic benefits now.
Formal verification is not that tool for most projects right now. Would instagram or even facebook be better off? Most people would, correctly, say no.
And ultimately in the end, nearly all software (including quite a bit of open source software!) is written in pursuit of business reasons, and has to answer to that.
I'd think the security of Facebook privacy settings will be improved by, for example, lightweight modelling using Alloy. Alloy would catch bugs like this one:
I just had a quick look at Alloy ([0]), and I'm interested in how it could be integrated into the software development process -- once you're confident about your Alloy model, you have to transfer it to working code somehow. I'd try to use both "fact" and "assert" statements from Alloy code as assertions in my production code (e.g. Python or Java). How is this usually done?
I did not say all software, just key components as it is pretty clearly laid out in the original article. I disagree with the significant resource aspect as well. I recommend Leslie Lamport's recent talk for some very lightweight ways to get started with formal verification: http://channel9.msdn.com/Events/Build/2014/3-642.
Furthermore, I think that you're ignoring that TDD tries to be a practical solution to certain real-world problems. This means that trade-offs are made in the name of creating software that works sufficiently well, while keeping expenses in check.
Sure, extensive formal verification of all software would probably bring some benefit in terms of correctness and perhaps security. But you're not considering the cost involved.
So far, such verification has only proven to be possible in rather limited situations, namely where there are significant resources available, or in academic exercises. Maybe this will change in the future, but in the present it's generally far more cost-effective to use a statically-typed programming language along with some form of automated testing. That gives many of the benefits of more formal methods of verification, but while also avoiding many of the costs, even if the end result doesn't conform to some theoretical idea of "perfection".