About one year ago Science Daily published an article about ongoig efforts to produce a new approach to software development, where programs can be mathematically proved to be bug-free:
Goodbye To Faulty Software?
http://www.sciencedaily.com/releases/2008/07/080716154355.htm
Will it ever be possible to buy software guaranteed to be free from bugs? A team of European researchers think so. Their work on the mathematical foundations of programming could one day revolutionise the software industry.
By the way, the Types Project mentioned in the article has its own page:
http://www.cs.chalmers.se/Cs/Research/Logic/Types/index.html
