London,European researchers are working on mathematical foundations of programming to create fault free software in the future.

People are remarkably tolerant of software that goes wrong, but when it comes to faulty cars or TV sets, they would insist that they be set right without much ado, the researchers said.

"The software industry is still very immature compared to other branches of engineering," says Bengt Nordström, computer scientist at Chalmers University, Göteborg.

"We want to see programming as an engineering discipline but it's not there yet. It's not based on good theory and we don't have good design methods to make sure that at each step we produce something that's correct."

Nordström is for rethinking the whole approach to software design. The usual approach is to validate a programme via a lengthy testing process. Instead, he would like to see a design philosophy that guarantees from first principles that a programme 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. It is not that simple, of course, but so promising is type theory that since 1989 the EU has been funding a string of projects to develop it under the 'Future and Emerging Technologies Programme'.

Nordström was coordinator of one of the projects, TYPES, which fosters co-operation on the topic among researchers at 15 European universities and research institutes, along with those at 19 associated academic and industrial organisations.

The TYPES partners are also releasing open source software packages that anyone can download, use and modify. These packages include several 'proof editors' that, in type theory, are the key to guaranteeing the correctness of programmes.

"European research in this field is the strongest in the world," Nordström pointed out. "Many computer programmes are going wrong, they don't work properly, and in the long run this research will help. This is a very slow process, it takes many years to get ideas from the universities into industry but I think it's slowly taking place."

Results from type theory are already finding their way into other projects. The EU-funded Mobius project is developing methods, known as 'proof-carrying code', for downloaded programmes to be certified as bug-free, reports Sciencealert.

Meanwhile, a France-based company is using ideas from type theory to design secure embedded computer systems such as those used for smart cards. Further research is also under way in Japan.

But type theory could also be important in the transport, defence and healthcare sectors, where mistakes can cost lives.

EMAIL THIS NEWS COMMENTS No comments yet