> a demonstration that any program in the hypothetical dialect that can invoke undefined behaviour either uses `unsafe` or is rejected by the borrow checker.

This isn’t quite what they’re doing here. They’re trying to define what guarantees the compiler should make about its treatment of unsafe code to strike a balance between usability and the ability of the compiler to optimize.