A small British firm shows that software bugs aren't inevitable (2005)

http://spectrum.ieee.org/computing/software/the-exterminators

by cjg • 11 years ago

55 60 11 years ago

spectrum.ieee.org

boothead• 11 years ago

Interesting read. I actually used the first Mondex system at Exeter Uni and it worked very well. Never knew why before :-)

taspeotis• 11 years ago

Related reading: how NASA does it [1].

[1] http://www.fastcompany.com/28121/they-write-right-stuff/

ckozlowski• 11 years ago

That was a fantastic read, thanks. =)

jaziek• 11 years ago

Interesting.

I think the point about the mathematics being too difficult for a "rank and file" programmer is probably a little off base. It isn't so much that the concepts are difficult as the fact that it seems prohibitively time consuming for relatively little gain that would put most people (especially those managing a project) off using formal specification / verification to build their software.

In most cases besides safety critical systems, it is acceptable to ship a product in 1/10th of the time, knowing that there is chance that there are imperfections.

Additionally, having used the Z language mentioned in the article, and taken some classes in university on formal methods, the thing which put me off the most was the (necessary) verbosity of the specification languages that are used for these type of things. I never wrote something that wasn't incredibly trivial, because it would have taken too long.

Jafit• 11 years ago

"1/10th of the time" implies that it takes 10 times longer to do the math than it does to stare at the screen with your head in your hands saying "oh god what have I done?" to yourself. I'd wager that's not the case.

DennisP• 11 years ago

As a rank and file programmer who didn't take university classes on formal methods, I've found it pretty difficult to dig up accessible tutorials.

mannykannot3• 11 years ago

This wasn't my introduction to these methods, but I wish it was:

http://www.amazon.com/Error-Free-Software-Know-How-Correctne...

mannykannot3• 11 years ago

It's a paradigm shift compared to the usual approach to programming, so I don't think it is for everybody, and realistically, it doesn't have to be.

For me, the most useful thing about learning some of this is that while I never, in practice, do fully formal proofs, I make informal arguments for correctness as I write and I think about what it would take to formalize them - what is the invariant, preconditions etc. here? For the tricky bits, I will write out an informal argument for correctness and include it as a comment.

According to the article, Praxis is not using formal proofs exclusively, or even predominately, and is using Z mainly for the precise expression of ideas, while keeping them free of unnecessary implementation detail (in other words, for abstraction.)

adrianN• 11 years ago

I think an important thing that we're currently missing is some kind of quantitative assessment what influence various measures have on software quality. All we have are "best practices" that all sound like common sense, but without much data backing them.

How much do formal methods really buy us it terms of quality? What's the defect rate if you use language X vs language Y? Is it better to spend lots of time gathering requirements and then produce something that exactly matches the requirements or is it better to iterate as quickly as possible and gather requirements as you go? What's the impact of the team as compared to the methodology?

I suspect the answers to these questions are really murky and its not clear whether there is a single methodology that produces the best quality for the money invested.

TheOtherHobbes• 11 years ago

Actually all we have is faddy unrigorous hobbyisms, mediocre tools, and poor management.

If everyone did what Praxis does software would work more reliably, but there would be far fewer programmers and - crucially - far fewer projects of all kinds.

We have the software industry we have because businesses don't want to pay for a better industry. It's the classic "worse is better" dilemma.

If software were rigorous, the initial cost of many projects would make them look prohibitively expensive. You can try to argue that total costs, including fixes and maintenance, are much lower, but not many managers are going to pay n times more for a project up front in the hope the cost will be n times less over its lifetime - even if there's a serious risk of paying millions or billions and literally getting nothing of use, as regularly happens on very big contracts.

Eventually quality would get cheaper. But for now it's as if the entire field is drowning in technical debt, buried under me-too frameworks and languages that do very little to genuinely improve productivity or reliability, supported by "Take the money, promise everything, and hope for the best" commercial attitudes.

Unfortunately you'd have to wipe out so many languages, techniques, ideas, systems, practices, and management attitudes, and put so many people out of work - or force them into retraining - that the kind of bug rates Praxis produce are never going to be possible across the industry as a whole.

HeyLaughingBoy• 11 years ago

Oh, we have those. The metrics gathered by a team doing TSP (https://en.wikipedia.org/wiki/Personal_software_process) are useful since the SEI (https://en.wikipedia.org/wiki/Software_Engineering_Institute) has data on thousands of projects and the metrics do provide good guidance when used appropriately. It is possible to consistently achieve < 0.1 defects/kloc using TSP.

The problem is, having spent seven years on a PSP/TSP team, that it greatly slows the development process so it's really only useful for those few types of projects where the cost of quality is worth it. For the vast majority of software, I'd say that it's better to accept a small number of minor defects in order to ship faster.

knappador3• 11 years ago

A referentially transparent, small function, has always been easy to write bug-free assuming the OS doesn't lose a page-table entry, a network interrupt isn't exploitable, and cosmic rays don't flip bits. The issue has never been that we can't write something that's correct.

Getting that correctness to propagate because of the strictness of all the tools involved and accuracy of their construction is the issue, which leaves us with needing to either automate proofs with Coq or prove things in more general ways that lead to undecidable problems etc. Still, the fact that one function can be written bug-free and known to be bug-free does indicate that it's not an inevitability of probability playing out as code grows.

We have null-pointer exceptions and no maybe type. The API's that emit nulls sometimes make me expect sewage to leak from light sockets. It's possible to do better. We just don't, and none of us love it. Rust and Kotlin are at least very exciting. I'd like to understand some Coq more in the context of x86. What routines are strictly necessary to even do Coq? A response based on some statement about how the Y-combinator enables X where X leads to Y would not surprise me.

detrino• 11 years ago

Small imperative functions are just as easy to make bug free, I don't buy it.

knappador3• 11 years ago

Also true. Still, purity (just part of referential transparency) should be highlighted as something that helps not just with the function you're writing , but also functions that need to call that function.

efaref3• 11 years ago

With nicer syntax, nulls are equivalent to Maybe types. Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.

skrebbel• 11 years ago

Equivalent at runtime, yes, but with less static type checking.

chriswarbo3• 11 years ago

With nicer syntax, nulls are equivalent to Maybe types.

No they're not, since you can't nest NULLs.

Say I have a database of "Users", with "birthdates" mapping a "User" to a "DateOfBirth" and "spouses" mapping a "User" to a "User", I can look up a User's DateOfBirth either using a Maybe or by allowing NULLs:

    -- Maybe
    getDOB :: User -> Maybe DateOfBirth

    -- Nullable
    getDOB :: User -> DateOfBirth

I can also look up a User's spouse with either a Maybe or a NULL:

    -- Maybe
    getSpouse :: User -> Maybe User

    -- Nullable
    getSpouse :: User -> User

So far they're pretty much equivalent. However, what if I want to look up a spouse's DateOfBirth?

    -- Maybe
    spouseDOB :: User -> Maybe (Maybe DateOfBirth)
    spouseDOB u = fmap getDOB (getSpouse u)

    -- Nullable
    spouseDOB :: User -> DateOfBirth
    spouseDOB u = let s = getSpouse u
                   in if s == NULL then NULL
                                   else getDOB s

These are no longer equivalent. In the Maybe case we can distinguish between three kinds of values:

- `Nothing` indicates that we can't find the spouse

- `Just Nothing` indicates that we can find the spouse but not the DOB

- `Just (Just x)` indicates that we found both the spouse and the DOB

In the nullable case we can only distinguish between two kinds of values:

- `NULL` indicates that either we couldn't find the spouse or we couldn't find the DOB, but we don't know which

- Anything else indicates that we found the spouse and the DOB

The Maybe approach gives us strictly more information; although we can choose to ignore it if we like, either by using `join` or by replacing `fmap` with `>>=` (AKA "bind", which is a combination of `fmap` and `join`).

dragonwriter• 11 years ago

With nicer syntax, nulls are equivalent to Maybe types.

In a language that lacks maybes, but has nulls, what is the equivalent of the type Maybe (Maybe Int)?

Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.

Even ignoring the lack of composability, flatMap is an operation on a broad category of which Maybe is one example; that generality is a key part of its utility. ?. is a special-case operation on nullables, if you want to use it on any of the other things that flatMap works on (e.g., lists), you need a different operation, so you can't build generic algorithms. So, its not substantively the equivalent of what Maybe provides in languages where maybe is part of some broader category of operations on which flatMap can be applied.

stevoski• 11 years ago

Even algorithms "proved" correct sometimes turn out to have bugs:

"I was shocked to learn that the binary search program that Bentley proved correct and subsequently tested in Chapter 5 of Programming Pearls contains a bug."

That's from Joshua Bloch's discovery in 2006 that Java's binary search implementation was broken: http://googleresearch.blogspot.com.es/2006/06/extra-extra-re...

efaref3• 11 years ago

Interesting. The bug in the proof is in the assumption that ints contain any integer and addition operates the same in normal mathematics, when in fact they're the set of values in [INT_MIN, INT_MAX] and addition has overflow behaviour.

Arguably addition (or any operation) that overflows with signed integers ought to cause some kind of SignedIntegerOverflow exception. If you want to do modulo mathematics in the set of [0, 2^n) then you should explictly use unsigned integers, which are defined to work that way.

pjc502• 11 years ago

I've been seriously considering doing a mini programming language where you can type-decorate numbers with exactly what behaviour you want and what their range is.

So you could have "integer, range [a-b), exception on overflow" or "integer, 32-bit, unsigned, wrap" or "integer, 8-bit, signed, saturates" (the latter is useful in codecs and often available in assembly).

georgerobinson• 11 years ago

Can you elaborate on this further?

Would this mean that Bentley's proof was in fact incorrect (i.e. not a valid proof at all) or that it simply didn't consider integer overflow for fixed size ints?

I wonder to what extent the implementation (i.e. the size of the integer type used) should affect the proof that an algorithm is correct?

pdpi• 11 years ago

The exact size doesn't matter nearly as much as the fact that it has a bounded size. That changes the algebraic structure your proof operates on — and proofs on finite fields are often either general or at least give you results that explicitly depend on the size of the underlying set.

chriswarbo3• 11 years ago

I suppose different people may answer your questions in different ways, depending on how they define words like "proof" and "correct". I would answer like this: the proof was correct, but it was solving the wrong problem (unbounded ints rather than bounded).

Inside a formal system it's relatively easy to understand what's going on; the real difficulties are at the boundaries: how do we build a formal model of a real system, and how do we translate formal results back to the original system? It's a lot like programming: manipulating data is easy, the problems are getting the right data and interpreting what the output means.

In this case, the model didn't capture overflow; so the proof is valid for that model, but it's not a useful model for Java's ints.

brodo• 11 years ago

There is a Google tech talk called "The Remote Agent Experiment: Debugging Code from 60 Million Miles Away" where the speaker describes how they did a proof that their code was deadlock free but it still ran into a deadlock. (I don't remember the details)

sqldba• 11 years ago

Link for the apathetic and disaffected https://www.youtube.com/watch?v=_gZK0tW8EhQ

PhantomGremlin• 11 years ago

I've seen that example before, but I don't like it. It's an example of fixed-point overflow, but it wouldn't occur in practice.

It would manifest itself with 32-bit integer indexes and with arrays of greater than 2^30 elements. So phooey. You can't even fit that many array elements into a 32-bit address space. And if you're in a 64-bit address space, you should be using 64-bit indexes.

Whine: way back in the 1960s, the IBM S/360 threw a fixed-point overflow exception (okay, to be pedantic, they called it a "program interruption", but it's the same idea) when you did that. Sadly, the Fortran compiler of the day masked it. And this same philosophy has carried over to today. About 99 times out of 100, fixed point overflow is bad, why is it being masked off?

andrewmu• 11 years ago

Java only allows signed 32-bit integers as array indices. It 's a compile time error to access an array with a long index (http://docs.oracle.com/javase/specs/jls/se8/html/jls-10.html...).

Alphasite_• 11 years ago

Not every language masks it, Swift certainly doesn't.

tekacs• 11 years ago

'Beware of bugs in the above code; I have only proved it correct, not tried it.' - Donald Knuth, 1977

bhrgunatha• 11 years ago

Maybe he probably proved the mathematical algorithm was correct. The problem is we have to implement algorithms using machines, which aren't perfect. They do a great job most of the time, but they exist in a physical environment which has restrictions and outside influences.

We can only work with the tools and techniques we've discovered so far. Later, we find situations or results that show our tools or techniques aren't correct or aren't good enough and we improve them to cover the new situations.

knappador3• 11 years ago

Safe points, jit, and VM all introduce extra layers of complexity. I bet it's definitely harder in the context of the JVM muddying up the picture.

gohrt• 11 years ago

Sure. You can trivially prove any algorithm is correct, if you abstract away enough details, where the devil lives.

osullivj• 11 years ago

LTU has a good discussion on Fetzer's classic critique of program verification: http://lambda-the-ultimate.org/node/2783

scorchio• 11 years ago

For engineers, the last paragraph is the most pertinent:

"The key weapon is abstraction," he says. "If you can build abstractions well enough, you should be able to break things down into bits you can handle." That maxim guides every other discipline in engineering, not least the design of computer hardware. Why not apply it to software, too?

andyjohnson02• 11 years ago

"Why not apply it to software, too?"

One the whole, we do. But sometimes abstractions leak [1]. Sometimes you get impedance mismatches when you try to layer them. Sometimes the abstraction isn't what you think it is or want it to be.

An example of the last point is alluded to in a comment by efaref about a binary search algorithm that turned-out to be broken because it assumed that an integer type in the implementation language behaved the same way as integers in mathematics, but it didn't because it didn't allow arbitrary-size values. The abstraction provided by the integer type was faulty.

[1] https://en.wikipedia.org/wiki/Leaky_abstraction

mannykannot3• 11 years ago

If one were using formal methods in these circumstances, they should, in principle, reveal those leaks and impedance mismatches to you (or, more precisely, reveal to you any problems they cause in your specific design.) The existence of leaks and impedance matches in informal abstractions is an argument for formality, not against it.

throwaway7767• 11 years ago

Can we change the title here? It's directly quoting the byline, but it contradicts the article.

Title/byline: "A small British firm shows that software bugs aren't inevitable (2005)"

Article: "Praxis doesn't claim it can make bug-free software, says Amey, now the company's chief technical officer. But he says the methodology pays off. Bugs are notoriously hard to count, and estimates of how common they are vary hugely. With an average of less than one error in every 10 000 lines of delivered code, however, Praxis claims a bug rate that is at least 50--and possibly as much as 1000--times better than the industry standard."

It's impressive, and I'd like to see more formal verification in software especially for security-critical components. But the title is factually incorrect.

dang• 11 years ago

I can't think of a better (more accurate and neutral) title right now, but if you or anyone suggests one, we can change it.

mamcx• 11 years ago

Note this:

""" Only after Praxis's engineers are sure that they have logically correct specifications written in Z do they start turning the statements into actual computer code. The programming language they used in this case, called Spark, was also selected for its precision. Spark, based on Ada, a programming language created in the 1970s and backed by the U.S. Department of Defense, was designed by Praxis to eliminate all expressions, functions, and notations that can make a program behave unpredictably. """

Is not only a problem that our industry lack discipline, is that almost everyone is so resistant to use better tools.

When some insist to use C++/JavaScript/PHP/MySql/Mongo/etc (tools with bad design/complexity/bug-prone/etc flaws) with the excuse that is possible to use them "well" if only we are more "disciplined" and "pay attention"?

When bad tools are bad, discipline is not the answer. Is fix the tool, or get rid of them.

Why developers understand that if a end-user have a high-error rate in one program is a problem with the program but when that happend with a language/tool for developers... not think the same???

A small British firm shows that software bugs aren't inevitable (2005)

Related Stories