Hacker News new | ask | show | jobs
by mhh__ 1878 days ago
Spectre isn't really something that you can catch with formal verification. It sort of isn't a bug, that's why it's such a problem.
1 comments

Only because most models focus on functionality, not on timing.
No it's because they focus on speed.

Eliminating spectre is either very hard or very slow. Of course you could verify that spectre does or doesn't happen formally, but at what cost?

You changed your argument flavor like a neutrino, used a false dilemma and had it swim with red herring. Don't take this as a harsh judgement but as something to work on.

There are ways to solve this now with type systems, dependent type systems, affine type systems, session types, etc. That allow us to track and prove what pieces of data should be visible (for many definitions) to whom.

We also will not know the cost unless we start designing our systems rigorously. Think of it as an accounting problem, and economics problem and engineering is made of up primarily as the combination of economics and failure analysis.

We have the means and methods to solve these problems now, we should use them.