Even algorithms "proved" correct sometimes turn out to have bugs:<p>"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."<p>That's from Joshua Bloch's discovery in 2006 that Java's binary search implementation was broken:
<a href="http://googleresearch.blogspot.com.es/2006/06/extra-extra-read-all-about-it-nearly.html" rel="nofollow">http://googleresearch.blogspot.com.es/2006/06/extra-extra-re...</a>
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.<p>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.<p>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.
Related reading: how NASA does it [1].<p>[1] <a href="http://www.fastcompany.com/28121/they-write-right-stuff/" rel="nofollow">http://www.fastcompany.com/28121/they-write-right-stuff/</a>
Interesting.<p>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.<p>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.<p>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.
Can we change the title here? It's directly quoting the byline, but it contradicts the article.<p>Title/byline: "A small British firm shows that software bugs aren't inevitable (2005)"<p>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."<p>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.
Note this:<p>"""
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.
"""<p>Is not only a problem that our industry lack discipline, is that almost everyone is so resistant to use better tools.<p>When some insist to use C++/JavaScript/PHP/MySql/Mongo/etc (tools with bad design/complexity/bug-prone/etc flaws) with the <i>excuse</i> that is possible to use them "well" <i>if only</i> we are more "disciplined" and "pay attention"?<p>When bad tools are bad, discipline is not the answer. Is <i>fix</i> the tool, or get rid of them.<p>Why developers understand that if a end-user have a high-error rate in one program is a problem <i>with the program</i> but when that happend with a language/tool for developers... not think the same???
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.<p>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?<p>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.
For engineers, the last paragraph is the most pertinent:<p>"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?
LTU has a good discussion on Fetzer's classic critique of program verification: <a href="http://lambda-the-ultimate.org/node/2783" rel="nofollow">http://lambda-the-ultimate.org/node/2783</a>