My survey of the computer science literature suggests there are only two economical ways to achieve extremely low defect rates (< 1 defect per K...
For further actions, you may consider blocking this person and/or reporting abuse
I've looked briefly into SPARK, because I also would prefer to avoid introducing mistakes. For now I use typed functional programming. An expressive type system along with pure functions in the money-making code (core business logic) surfaces most errors at design-time. This allows me to avoid it even being possible for data to be in a wrong state. Also property-based testing goes a long way to ensuring the logic handles unexpected inputs properly. (I mainly use standard unit tests against the logic so far. I've been meaning to get into property-based.) Outside of sensitive areas which require formal verification, for me this is enough to prevent most of the mechanical errors of software dev.
So now the problem remains (even if I used formal verification) that sometimes I do a pretty decent job of developing the wrong thing. This is usually even more wasteful than doing something mechanically wrong. This is very common when devs implement "exactly what was asked". The main mitigation is instead of implementing the requested solution, dig deeper to find out the problem that the stakeholder is having, and address that. This can be difficult (to secure stakeholder time, to communicate effectively, etc).
I've shared this before. I had a situation recently where a customer asked for "just a field" added to an entity. But when we dug a little deeper, the field by itself wasn't going to solve the problem they had. We proposed an alternative that was more work, but would directly address the problem. They were pleased with our proposal. And it turned out to be a feature that other customers also wanted. Had we added just the field, it would have become unused cruft.
Thanks for sharing your experiences, Kasey.
Some functional languages (or subsets) can be formally proved/verified for correctness but I don't know much about that.
I love Quickcheck for property-based testing. We don't have a lot of code where it's a good fit but we have a few property-based tests in PHP. However, Quickcheck is much more powerful in a functional language. The minimum counter-example is particularly helpful in exposing errors in an easily digestible form.
Building the wrong thing is always a risk (even if you do careful requirements gathering and analysis). And if you took 5x more time to build it properly/correctly/carefully, it stings that much more when you find out that nobody needs what you built.
I've had experiences similar to yours where the customer presents his solution to the problem. And I've been burned by not digging deeper too. I've saved myself a lot of grief over the years when I started asking "what exactly are you trying to accomplish" when a customer presents a solution instead of a need/problem.
This is interresting and I think you'll learn lot of good things there.
But I'd say at least the language solve only part of the problem. It solve the problem of ensuring that the program you wrote actually does what you told the machine.
It doesn't ensure that you told the machine the right thing about what the program shall be doing from the specifications. It doesn't ensure neither that you understood the real problem you are trying to solve and managed to correctly translate the real world problem into a correct set of specifications...
That last one thing is responsible of 30-45% of all defects in a software and theses kind of defect, actually design defects are among the most costly to solve. In many places people don't even want to accept them as defects... But the real thing stil doesn't solve the real world problem even if it conform to the specs.
I totally agree.
The NASA study I mentioned in the post (also here) shows that the cost of missing or incorrect requirements can be devastating to a project because the costs rise exponentially the longer the defect is in the system.
I restricted my post to coding concerns but getting requirements right is super important too. I'm reading "Software Requirements" by Karl E Wiegers right now and I might write a post on that when I'm done.
Interesting food for thought! I like your dual approach of "better process" and "better language".
What are the safer languages out there?
I like to think Safe-D (a safer subset of the D programming language) is safer. But it is not ultra-safe in the complete and comprehensive static analysis sense that SPARK 2014 can claim.
Thanks.
There are different ways to think about safety. Languages that have automatic bounds checking for example are safer than those without (Java vs C).
Another aspect is whether the language can be proven formally. SPARK is one example and I believe I read that several of the functional languages (or subsets of them) are formally provable.
I read an article that said that Airbus is experimenting with model-driven development for critical systems because making sure that even Ada was correct was too difficult and costly. So, they just want to build a model and have software convert it into correct source code. Obviously that's a very specialized use case that's unlikely to gain widespread use in the near future.
Here's a link to AdaCore's product that might be similar to what Airbus is doing (code generation tools are over my head): adacore.com/qgen