What's really needed is a mathematical analysis of size of the bug space compared to the size of proving code required to cover it. I.e. to get to 99.5% confide

What's really needed is a mathematical analysis of size of the bug space compared to the size of proving code required to cover it. I.e. to get to 99.5% confidence that a system of size N is bug-free it would take a proving system of size f(N). Is f polynomial, a small exponent, a large exponent? If it's a large exponent, then the more you take on, the farther you get from your goal, and the narrowly targeted efforts are the best we can do.