alt Hacker NewsYou can't formally verify the soundness of something that inherently necessarily relies on hardware implementations that themselves could be faulty.
Replies
altairprime • yesterday at 9:39 PM
You can certainly verify the soundness of what is within your control, the compiler code, which is what is being suggested above.
LoganDark • yesterday at 9:40 PM
You can formally verify that the algorithm has the desired properties, though. If the hardware requires additional properties for soundness, then that would only be an error in the properties, not in the proof. (Of course, that would no longer prove soundness on that hardware.)
You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)