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.
We have become used to the idea that software will not work properly. While we would take a faulty car back to the dealer and demand they put it right, we are remarkably tolerant of software that goes wrong.
Nordström believes that the whole approach to software design needs to be rethought. The usual approach is to validate a program via a lengthy testing process. Instead, he would like to see a design philosophy that guarantees from first principles that a program will do what it says on the box.
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.
