> Here I refer to the typical modern interpretation of UB: assumptions the compiler may trust, without bounds on what happens if they are violated.
Makes that abundantly clear.
This basic realization opens up many avenues for interdisciplinary research. For example, maybe all the ink spill on "paraconsistent logics" will finally be useful for designing an unsafe language like C. (https://plato.stanford.edu/entries/logic-paraconsistent/ https://ncatlab.org/nlab/show/paraconsistent+logic .) Maybe "unsafe" in Rust is best understood as a logical "mode" of some sort. Lattice of allowed behaviors lead to a nice fine-grained semantics for semi-defined behavior.
I honestly don't know whether no one talks about this because it is very obvious to researchers in the field, or because no one actually dove deep into this interpretation.