It seems to me that the arguments here are fair, but maybe the conclusion isn't. But the guarantees that we expect are much stronger than a correct protocol, h

It seems to me that the arguments here are fair, but maybe the conclusion isn't. But the guarantees that we expect are much stronger than a correct protocol, handshake, or compiler optimization. We need the entire system to be reliable, and we need proof effort to be minimal for widespread adoption to be feasible. Ideally, yes, of course that is true. But even if it is not currently true, having some aspects of a system formally proven still means we can focus our limited resources on the other aspects and the integration, and that's still beneficial.