“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 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. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct.
More HERE.
