It's possible to write flaw-free software, so why don't we?

It's possible to write flaw-free software, so why don't we?
If Spock would not think it illogical, it’s probably good code. Credit: Alexandre Buisse, CC BY-SA

Legendary Dutch computer scientist Edsger W Dijkstra famously remarked that "testing shows the presence, not the absence of bugs". In fact the only definitive way to establish that software is correct and bug-free is through mathematics.

It has long been known that software is hard to get right. Since Friedrich L Bauer organised the very first conference on "software engineering" in 1968, computer scientists have devised methodologies to structure and guide software development. One of these, sometimes called strong or more usually formal methods, uses mathematics to ensure error-free programming.

As the economy becomes ever more computerised and entwined with the internet, flaws and bugs in software increasingly lead to economic costs from fraud and loss. But despite having heard expert evidence that echoed Dijkstra's words and emphasises the need for the correct, verified software that formal methods can achieve, the UK government seems not to have got the message.

Formal software engineering

The UK has always been big in formal methods. Two British computer scientists, Tony Hoare (Oxford 1977-, Microsoft Research 1999-) and the late Robin Milner (Edinburgh 1973-95, Cambridge 1995-2001) were given Turing Awards – the computing equivalent of the Nobel Prize – for their work in formal methods.

British computer scientist Cliff B Jones was one of the inventors of the Vienna Development Method while working for IBM in Vienna, and IBM UK and Oxford University Computing Laboratory, led by Tony Hoare, won a Queen's Award for Technological Achievement for their work to formalise IBM's CICS software. In the process they further developed the Z notation which has become one of the major formal methods.

The formal method process entails describing what the program is supposed to do using logical and mathematical notation, then using logical and mathematical proofs to verify that the program indeed does what it should. For example, the following Hoare logic formula describing a program's function shows how formal methods reduce code to something as irreducibly true or false as 1 + 1 = 2.

It's possible to write flaw-free software, so why don't we?
Hoare logic formula: if a program S started in a state satisfying P takes us to a state satisfying Q, and program T takes us from Q to R, then first doing S and then T takes us from P to R.

Taught at most UK universities since the mid-1980s, formal methods have seen considerable use by industry in safety-critical systems. Recent advances have reached a point where formal methods' capacity to check and verify code can be applied at scale with powerful automated tools.

Government gets the message

Is there any impetus to see them used more widely, however? When the Home Affairs Committee took evidence in its E-crime enquiry in April 2013, Professor Jim Norton, former chair of the British Computer Society, told the committee:

We need better software, and we know how to write software very much better than we actually do in practice in most cases today… We do not use the formal mathematical methods that we have available, which we have had for 40 years, to produce better software.

Based on Norton's evidence, the committee put forward in recommendation 32 "that software for key infrastructure be provably secure, by using mathematical approaches to writing code."

Two months later in June, the Science and Technology Committee took evidence on the Digital by Default programme of internet-delivered public services. One invited expert was Dr Martyn Thomas, founder of Praxis, one of the most prominent companies using formal methods for safety-critical systems development. Asked how to achieve the required levels of security, he replied that:

Heroic amounts of testing won't give you a high degree of confidence that things are correct or have the properties you expect… it has to be done by analysis. That means the software has to be written in such a way that it can be analysed, and that is a big change to the way the industry currently works.

The committee sent an open letter to cabinet secretary Francis Maude in asking whether the government "was confident that software developed meets the highest engineering standards."

Trustworthy software is the answer

The government, in its response to the E-crime report in October 2013 , stated:

The government supports Home Affairs Committee recommendation 32. To this end the government has invested in the Trustworthy Software Initiative, a public/private partnership initiative to develop guidance and information on secure and trustworthy software development.

This sounded very hopeful. Maude's reply to the Science and Technology committee that month was not published until October 2014, but stated much the same thing.

So one might guess that the TSI had been set up specifically to address the committee's recommendation, but this turns out not to be the case. The TSI was established in 2011, in response to governmental concerns over (cyber) security. Its "initiation phase" in which it drew from academic expertise on trustworthy software ended in August 2014 with the production of a guide entitled the Trustworthy Security Framework, available as British Standards Institute standard PAS 754:2014.

This is a very valuable collection of risk-based software engineering practices for designing trustworthy software (and not, incidentally, the "agile, iterative and user-centric" practices described in the Digital by Default service manual). But so far formal methods have been given no role in this. In a keynote address at the 2012 BCS Software Quality Metrics conference, TSI director Ian Bryant gave formal methods no more than a passing mention as a "technical approach to risk management".

So the UK government has been twice advised to use mathematics and formal methods to ensure software correctness, but having twice indicated that the TSI is its vehicle for achieving this, nothing has happened. Testing times for correctness, then, something that will continue for as long as it takes for Dijkstra's message to sink in.

Explore further

Games help improve software security

This story is published courtesy of The Conversation (under Creative Commons-Attribution/No derivatives).
The Conversation

Citation: It's possible to write flaw-free software, so why don't we? (2014, November 11) retrieved 18 October 2019 from
This document is subject to copyright. Apart from any fair dealing for the purpose of private study or research, no part may be reproduced without the written permission. The content is provided for information purposes only.

Feedback to editors

User comments

Nov 11, 2014
The problem is that real software that runs under real operating systems cannot guarantee for itself that it always goes from state P to Q, because the software is relying on underlying system calls which may or may not produce the desired behaviour.

The software library you're calling may not operate in the specified and documented way, or the required library in the user's system has been substituted with a different version that behaves in subtly different ways. Even the automatic compiler optimizations used to turn out the binaries can sometimes cause differences in behaviour, so it's impossible to know whether the fault is in your code, in the other guy's code, or neither. Then there's even hardware bugs!

Much of practical programming is coding around other peoples' errors, and so any rigorous proof that it works is as soon false as the first operating system update arrives.

Nov 11, 2014
While intellectually interesting, and perhaps practical once AI becomes a reality to do the heavy lifting... In almost 20 years of software engineering consulting I have never encountered a commercial client who would be willing to pay for the massive overhead costs associated with producing bug free software. It's a non-starter, and a slightly ridiculous idea. Theoretically we can make cars so strong and insulating that no one would die in an auto accident, but do we? Are we striving for that? No, of course not. We understand (those who bother thinking about it at all) that the massive costs, resources spent, and severe limitations of use would damage society more than it would help. So too with this. The Apple and Android stores would drop from hundreds of thousands of apps to perhaps a few dozen banking apps. And society has decided (quite rightly) that it's more important that we have thousands of buggy farting apps. Vive la société! (sp?)

Nov 11, 2014
The title of this article is not strictly a lie. It will be possible. But it is not possible right now for any type of complex or truly interesting software. It is also not at all feasible under our current software development models. Eikka is also spot about the OS, and even in cases where specialized narrow-focus operating systems are created from scratch (but also probably in C which is half the problem), they are still entirely full of bugs. Firmware is almost always shit too. Even the hardware can have its problems. What they are talking about just isn't going to happen anytime soon.

Also, I see the government is helping develop this. I was involved in developing medical software with state of california at one point. I don't have a good feeling about how this will turn out.

Nov 12, 2014
It's possible to build roads that will endure for 30+ years, so why don't we?

Software is written to satisfy a range of requirements. Working correctly (all of the time) is only one requirement that only might be present. Often the requirements themselves are a shifting sand hill. Welcome to the real world.

Nov 15, 2014
It's possible to build roads that will endure for 30+ years, so why don't we?

Is it really?

Nov 16, 2014
There are flaws because there are deadlines, profit-oriented soft, no time for excellency.
No mistery at all.

Nov 16, 2014
I'm not an expert in software but what about the use of programming languages that can eliminate a lot of bugs? I'm thinking about Haskell.

Please sign in to add a comment. Registration is free, and takes less than a minute. Read more