@david_chisnall @mario "At no point in certified software development will anyone sign of on (for example) the C compiler's output being a 100% faithful representation of the C abstract machine."
This is quite the straw man you've summoned. Didn't get any better either.
Later.
Jul 29, 2026, 2:36 PMI don't know what you think you're arguing with, but that's exactly the claim that you were making. You seem to be confusing formal verification with... something?
@david_chisnall @mario No dude. You completely made it up.
Jul 29, 2026, 2:38 PMI can only assume you're not reading the thread in context because you jumped into a middle of a conversation with a post about a problem with the concrete machine not being a faithful representation of the abstract machine that the proofs were constructed in to say that, in certified software development, people signed off on that.