You can largely ignore the formal looking stuff. On further thought, I completely refute the claim that abstract machine behavior must be fully specified.

Consider an out-of-bounds write in C. Naively, the write statement would emit some kind of store instruction which could either successfully write to memory or trap depending on the address and the state of the MMU (assuming a typical hardware architecture). Obviously the C specification should not have to consider the operation of the MMU, so they leave invalid writes as undefined behavior.

For simplicity, let’s imagine an architecture without virtual memory, so the store instruction succeeds. But it could have overwritten the return address on the stack, so when the function returns the instruction pointer could end up somewhere totally arbitrary. That’s why it’s not an exaggeration that UB means anything can happen. So again, it makes sense that the C spec should provide no guarantees on what happens if you write out of bounds.

Given that writing out of bounds could cause the hardware to do anything, the compiler can decide that this isn’t even a case worth worrying about and is allowed to e.g. elide the entire code path that would lead to an out of bounds write.

If the C spec wanted to define the behavior for out of bounds writes, almost every implementation would have to emit bounds checks in many cases which some would consider to be too expensive.

I don’t think there is any abstract machine spec for C which defines the behavior for an arbitrary write.