By corollary does that mean that if there isn't a formal proof of how C compiles to assembly, and how those opcodes are interpreted by a particular CPU model, that C formally isn't specified to have any meaning to a CPU?
There are formally verified CPUs, they're just not the lovely high performance ones you probably want.
For what it's worth, this is a common sentiment people have when they first come to blows with formal. "If you can't verify everything, why verify anything?" is a reasonable question to ask but it's not a practical position to hold since formal does increase the quality of software/hardware. Don't argue for less formal, fight for more!
That would get you to the assembly generated, but not the behavior of the CPU in the question, which goes to show it's a pretty silly position to hold.
Undefined Behaviour in C is the opposite of a gap in the standard. It's behaviour that's addressed in the standard that for historic, political, and performance reasons is allowed to be inconsistent. That's the reason it sucks to have been bitten by it (e.g. to find out that shifting N-1 bits out of an N sized integer gives you 0 bits, but shift that Nth bit and all bets are off)
Yes? The combination of "historic, political, and performance" is a particular choice. Our attitudes to all of these are different to when C was maturing, particularly where reliability and security are involved.
And not least of all, we've learned more about programming language development than when C was created.
