Bug free software to come from EU open source Type Theory project
Will it ever be possible to buy bug-free software? A team of European researchers believes so – if the basis of primary programming is rethought.
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.”
