There are methods that can be applied to software that formally prove properties of software so that those pieces are free of bugs. These are called formal methods and require heavy use of math. Some of them are ASM and Z.
There are provers that help as well, such as Alloy.
For the typically/average project put there, the mayor problem I see is that people still rely on code coverage as the one and only metric for quality of their tests (if they even implement tests at all).
Code coverage is a lazy, flimsy and unreliable metric that has been subsumed by the more powerful metric called mutation score.
If devs utilized mutation analysis more, they would provably have much better quality software.
There are provers that help as well, such as Alloy.
For the typically/average project put there, the mayor problem I see is that people still rely on code coverage as the one and only metric for quality of their tests (if they even implement tests at all). Code coverage is a lazy, flimsy and unreliable metric that has been subsumed by the more powerful metric called mutation score.
If devs utilized mutation analysis more, they would provably have much better quality software.
See this video: http://confreaks.tv/videos/mwrc2014-re-thinking-regression-t...
And here: https://en.m.wikipedia.org/wiki/Mutation_testing