Bug free software to come from EU open source Type Theory project

“The software industry is still very immature compared to other branches of engineering,” says Dr Bengt Nordström, a computer scientist at Chalmers University in 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 believes the whole approach to software design needs to be rethought from the ground up. The usual approach is to validate programs through lengthy regression testing. Instead, he advocates a design philosophy that guarantees, from first principles, that a program will do what it says on the tin. And the key, he says is a mathematical approach called ‘type theory’ (funded by the EU since 1989), in which the specification for a computational task is stated as a theorem. The program that performs the computation is equivalent to the proof of the theorem – and is hence always correct. Nordström was coordinator of the EU type theory project, dubbed TYPES, whose partners are now releasing open source software for download, use and modification. “European research in this field is the strongest in the world,” insists Nordström. “Many computer programs are going wrong, and in the long run this research will help. This is a very slow process: it takes many years to get ideas from university into industry, but I think it’s taking place.”