Goodbye to faulty software?

This article I discovered via ACM entitled "Goodbye to faulty software?" highlights how often researchers just don't "get it". Here are a few key quotes:

"Will it ever be possible to buy software guaranteed to be free from bugs? A team of European researchers think so."

"The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct."

While they've been working on this "type theory" concept since 1989, I can't see how it's going to ever create a golden age of well designed software. Most problems with software are not that some technical bug causes it to fail, but that it has poorly conceived and poorly design features and functions. It's not bad code...it's bad design that's the problem. Still, some engineers fail to recognize that software serves humans, often in many varying situations, organizations, locales and cultures, and therefore is a much more complex and difficult challenge than building a simple bridge (one locale, simple, clear purpose and very few "use cases").

Matematics and engineering are great, and important to creating good software...but psychology, human factors and Design are pieces of the puzzle that can't be overlooked.

Nevertheless, when you're applying for grants, I'm sure it sounds better if you assert that your Math theory is going to save the world from bad software.