That is unlikely. For computational complexity theory reasons, writing correct software is extremely computationally expensive (regardless of whether or not the language is Turing complete). In fact, it is "the hardest problem in computer science", in the sense that any problem with bounded complexity can be efficiently reduced to software verification. Even verifying finite-state-machines (the simplest computational model) is PSPACE-hard.
What we can do is find many ad hoc ways, each helping to some extent with some kinds of correctness properties.
NASA with the Space Shuttle software came pretty close. http://history.nasa.gov/computers/Ch4-5.html
But enough money and the goal of making it infinitely flexible, having all the possible features, or the most perfect UX that a team can not decide on what it is will only make the software more bloated than it's reasonable, and fill it with bugs.
Of course, making mistakes is only human, but mistakes should never get past the build process (compilation, automated testing). Any mistake that does reflects an error in your design (not making your code amenable to verification) and/or your process (not capturing requirements in tests).
According to empirical studies, practicing TDD leads to a 90% (yes, that number is correct) post-ship bug reduction at an upfront cost of 15-35% more development time.
Which seems like a pretty good tradeoff, to me. (And I've experienced it firsthand.)
http://research.microsoft.com/en-us/groups/ese/nagappan_tdd....
Also discussed in this infoq article
http://www.infoq.com/news/2009/03/TDD-Improves-Quality
Here's someone's thesis paper on it, with data:
http://www.nomachetejuggling.com/files/tdd_thesis.pdf
There's also interesting discussions like this
http://programmers.stackexchange.com/questions/206355/the-re...
"it is my experience that the value proposition for TDD grows exponentially as the time and resources involved in a project grows linearly."
This has also been my own experience.
This person's comment also is interesting and has data
http://programmers.stackexchange.com/a/210756
Some of the above is empirical (read: scientific, no-bullshit) data.
My opinion on it has grown to the point that I think TDD should literally be inseparable from programming, and the two together should simply be called, "programming." Lacking any unit tests whatsoever (TDD or otherwise) should be called, "taking stupid, extremely hazardous risks to save a little time, like reading your phone while driving"
I've not found a programming task in at least 5 years that wasn't waaaay better-written when done via TDD. Some things, like IO, can be a challenge to unit-test, but that's why we have great ideas to solve that like Gary Bernhardt's awesome "Boundaries" talk https://www.youtube.com/watch?v=yTkzNHF6rMs
Yes. It's pretty easy to write provably correct software, just expensive.
> Developers are often guilty of just refactoring for no particularly good reason other than their personal sense of aesthetic, which can lead to endless (and destructive) refactoring
Not my experience, but even if so, if you require your software to be proven correct then it won't matter - any refactor that breaks it simply won't be accepted.
> More money also makes people design lazy, so that instead of finding clever ways to reduce effort and improve uniformity, you just have everyone make their own forms.
Um what? What does this have to do with anything?
There are lots of good reasons to refactor - if indeed frivolous refactoring is more prevalent I would think this kind of opinion should be supported by a source/reference.