4 ms·

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.

• amelius 6y ago
  Only because most models focus on functionality, not on timing.
  • mhh__ 6y ago
    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?
    • sitkack 6y ago
      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.