> There is a period of chaos where your prediction will play out over and over, but eventually there's a new equilibrium where it's just different rocks to look under.
When we take steps to eliminate classes of vulnerabilities, well, those vulnerabilities stop being a problem, and we're all more secure. For example, code written in Java or C# is immune from the buffer-overflow attacks, and use-after-free attacks, that continue to plague C code.
There was no counterweight built into this. Security was simply improved.
> Then people get bored again and they fall behind on upgrades, and now every time new functionality is added to the formal system, by definition people using the old version aren't getting that protection, so you'd look there first.
Failure to update packages causes security issues, yes. That doesn't mean that security improvements don't, well, improve security, overall. They absolutely do.
> If the rate of bugs (or maybe you call them features?) is negligible after a brief flurry of initial activity, then most of my argument collapses in a divide by zero error.
If they're using formal methods, they won't be adding bugs. (Discounting side-channel issues.)
I believe it's pretty unusual to see a company make non-verified changes to a codebase originally derived through formal methods. If they care about formal verification, they'll probably stick with it as they make changes.
> how valuable is breaking into a boring system? It's definitely not zero, because you've created another resource for yourself.
Sure - botnets.
> Doesn't code that runs on a lot of systems get far more attention than code that runs on a few?
Of course, but I'm not seeing what you're getting at here.