It is about solidifying semantics, but those semantics are still a concern to regular users who are writing `unsafe` code, not just Miri.

As I understand it, Miri would like to be certain about the presence/absence of the UB of any particular program execution, but there will probably always be some cases it can't catch.