I interpreted the comment a bit more generously that you did. You're absolutely corrent that it's possible, and I'll go as far as to say even desireable, to write provable correct code. However, I've never seen a demonstration of probably correct hardware. I interpreted the comment as reminder that even binary is, ultimately, a leaky abstraction.

I used to work in a facility where they'd test systems for radiation hardness. Get the system running, then shoot a proton beam travelling a significant fraction of the speed of light directly at the processor. It doesn't matter if the code was proven correct Dijkstra, it will eventually manifest bugs under these conditions.