The US National Security Agency has released a case study showing how to develop zero-defect code in a cost-effective manner. Diomidis D. Spinellis has taken a closer look at the claims and the code released for this project. At first when I read through the article I agree with most his points, but it gets quite interesting when I read the comments.
The things we consider important when living in our business-entrepriecey-systems-world might not be feasible when you’re doing realtime-secure-flightsystems etc. If you are working under the paradigm of formal verification, loops might be a bad thing.
I don’t know much about this stuff, and I am quite content not needing to think about it. That said I really try to strive for zero-defect, maintainable code, it just doesn’t seem worth it doing formal verification on most systems I work on. I should look into it though to learn a little about it without picking it up. I think working in this fashion will probably block all attempts to be agile.