It depends on what you mean by "safely". The spectre family of exploits has no general solution and requires specific mitigations. Aside from that, Wasm provides a sandbox that disallows escaping from it. That does leave scribbling on memory inside the sandbox, which is what this paper focuses on.

So for many use cases Wasm does allow what you mention, running unsafe code quickly on normal hardware, and it is being used in production for that purpose.

Note that they didn't break out of the sandbox. So this can't do anything bad to the machine it's running on.

Proof-carrying code? It, too, is old news.

Formal proofs can probably show that spectre and meltdown aren't exploited by enforcing type-safety for all speculative memory accesses, but that requires at least some knowledge of the target processor and may still be slower at processing untrusted input.

There's very little that can be done about rowhammer with formal methods because it breaks the assumptions of any formal model of computation (that values stored to RAM are the same values that will be eventually read from RAM).