Since there was a post about Spectre on the HN front page today, I wonder if HDLs should perhaps contain more formal verification tools; is that on the roadmap?
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?
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.
While this is still a long-term goal, I am planning to experiment how formal verification can be used in Racket-based hardware tools.