Because chances are the the formal spec itself won't be perfect. But even if it is you still have to worry about every layer below you in the software stack on top of the hardware. You might do everything perfectly at great cost and it all gets rendered moot by spectre/meltdown/rowhammer etc.

>Because chances are the the formal spec itself won't be perfect

It's not about creating 'perfect software', but about holding developers accountable. If a customer accepts a contract with a faulty spec, that's on them, not the developer.

>But even if it is you still have to worry about every layer below you in the software stack on top of the hardware. You might do everything perfectly at great cost and it all gets rendered moot by spectre/meltdown/rowhammer etc.

So what? It's not your fault. There's only one party that should be held liable for spectre, Intel.

But it aldo affects mainframes, no?

Well, it also affects certain AMD and ARM processors as far as I know, I was just talking about a specific example. If software can be exploited because of a bug in hardware, I think it only makes sense to assign liability to the hardware company.

But how would you know this? All you know is that the 'software' was compromised and the data leaked. Do you think the initial blame will go to the right place or just the company after all? You won't always figure out how something was definitely compromised. You'll look around and definitely find bugs in the software though.

>But how would you know this?

Well, if you have formally verified your system, you know that if the underlying systems work correctly, your work will correctly adhere to the spec. So if a breach occurs, there's two options - either the spec was bad or there's a hardware/OS/library bug.

Otherwise, you can't always know it, that doesn't strike me as a realistic goal in the first place. It's not about always being able to perfectly assign liability - obviously if you can't figure out how something was compromised, you simply can't assign any liability. But one could investigate and if you find deviations from the spec, you know where to correctly place blame.

>You'll look around and definitely find bugs in the software though.

If these are deviations from the spec, I think it would only be right to hold the developer liable. If a developer doesn't want this to occur, they could instead formally verify their software.

If the bugs are in the spec instead, the blame should lie with the party that accepted the spec.