8 ms·

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

55 points by cjg 11y ago

boothead 11y ago
Interesting read. I actually used the first Mondex system at Exeter Uni and it worked very well. Never knew why before :-)
taspeotis 11y ago
Related reading: how NASA does it [1]. [1] http://www.fastcompany.com/28121/they-write-right-stuff/ http://www.fastcompany.com/28121/they-write-right-stuff/
- ckozlowski 11y ago
  That was a fantastic read, thanks. =)
jaziek 11y 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 11y 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 11y 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.
  - mannykannot 11y ago
    This wasn't my introduction to these methods, but I wish it was: http://www.amazon.com/Error-Free-Software-Know-How-Correctness-Engineering/dp/0471930164 http://www.amazon.com/Error-Free-Software-Know-How-Correctne...
- mannykannot 11y 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 11y 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 11y 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 11y ago
  Oh, we have those. The metrics gathered by a team doing TSP (https://en.wikipedia.org/wiki/Personal_software_process https://en.wikipedia.org/wiki/Personal_software_process) are useful since the SEI (https://en.wikipedia.org/wiki/Software_Engineering_Institute 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.
knappador 11y 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.
- efaref 11y ago
  With nicer syntax, nulls are equivalent to Maybe types. Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.
  - skrebbel 11y ago
    Equivalent at runtime, yes, but with less static type checking.
  - chriswarbo 11y 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`).
stevoski 11y 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-read-all-about-it-nearly.html http://googleresearch.blogspot.com.es/2006/06/extra-extra-re...
- efaref 11y 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.
  - pjc50 11y 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).
    - revelation 11y ago
      I think they call that Ada. (not sure on the overflow behavior, but ranges are in)
      - AndyMcConachie 11y ago
        You might also argue that SQL shares some of these characteristics.
osullivj 11y ago
LTU has a good discussion on Fetzer's classic critique of program verification: http://lambda-the-ultimate.org/node/2783 http://lambda-the-ultimate.org/node/2783
scorchio 11y 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?
- andyjohnson0 11y 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 https://en.wikipedia.org/wiki/Leaky_abstraction
  - mannykannot 11y 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.
    - andyjohnson0 11y ago
      I agree in principle, although in practice I am sceptical about the practicality of applying formal methods to large systems. The ratio of effort to reward just seems too large for most domains.
throwaway7767 11y 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 11y 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 11y 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???

55 points by cjg 11y ago

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

taspeotis 11y ago

Related reading: how NASA does it [1]. [1] http://www.fastcompany.com/28121/they-write-right-stuff/ http://www.fastcompany.com/28121/they-write-right-stuff/

ckozlowski 11y ago
That was a fantastic read, thanks. =)

jaziek 11y 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 11y 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 11y 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.
- mannykannot 11y ago
  This wasn't my introduction to these methods, but I wish it was: http://www.amazon.com/Error-Free-Software-Know-How-Correctness-Engineering/dp/0471930164 http://www.amazon.com/Error-Free-Software-Know-How-Correctne...
mannykannot 11y 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 11y 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 11y 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 11y ago
Oh, we have those. The metrics gathered by a team doing TSP (https://en.wikipedia.org/wiki/Personal_software_process https://en.wikipedia.org/wiki/Personal_software_process) are useful since the SEI (https://en.wikipedia.org/wiki/Software_Engineering_Institute 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.

knappador 11y 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.

efaref 11y ago
With nicer syntax, nulls are equivalent to Maybe types. Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.
- skrebbel 11y ago
  Equivalent at runtime, yes, but with less static type checking.
- chriswarbo 11y 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`).

stevoski 11y 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-read-all-about-it-nearly.html http://googleresearch.blogspot.com.es/2006/06/extra-extra-re...

efaref 11y 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.
- pjc50 11y 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).
  - revelation 11y ago
    I think they call that Ada. (not sure on the overflow behavior, but ranges are in)
    - AndyMcConachie 11y ago
      You might also argue that SQL shares some of these characteristics.

osullivj 11y ago

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

scorchio 11y 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?

andyjohnson0 11y 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 https://en.wikipedia.org/wiki/Leaky_abstraction
- mannykannot 11y 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.
  - andyjohnson0 11y ago
    I agree in principle, although in practice I am sceptical about the practicality of applying formal methods to large systems. The ratio of effort to reward just seems too large for most domains.

throwaway7767 11y 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 11y 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 11y 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???