ACM TechNews

Goodbye to Faulty Software?

ICT Results (07/15/08)

A team of European researchers believes that it will be possible to create software that is guaranteed to be free from bugs. "The software industry is still very immature compared to other branches of engineering," says Chalmers University computer scientist Bengt Nordstrom. Nordstrom believes the entire approach to software design needs to be rethought, replacing the usual approach of validating a program through a lengthy testing process with a design philosophy that guarantees from first principles that a program will act as it should. The key is a reformation of mathematics called type theory based on the notion of computation, in which the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is essentially the proof of the theorem, and by proving the theorem the program is guaranteed to be correct. The European Union has funded a series of projects to develop type theory since 1989. Nordstrom was coordinator of the TYPES project, which supported cooperation on type theory between researchers at 15 European universities and research institutes and 19 associated academic and industrial organizations. TYPES has released several open source programs, including proof editors that, in type theory, are the key to guaranteeing bug-free programs. "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," Nordstrom says.

http://cordis.europa.eu/ictresults/index.cfm/section/news/tpl/article/
BrowsingType/Features/ID/89864

---

© Copyright 2008 Information, Inc. This service may be reproduced for internal distribution.