What does `unsafe` mean?

Thanks @alercah for these very interesting thoughts! Let me just comment on one thing. :slight_smile:

I would say there is a technical point, and you have hinted at it later: UB is the part of the API contract that the compiler knows about. The compiler has been taught to assume that its input program is UB-free, and that is exploited all over the place for the purpose of optimizations. You are admitting this later in your post, but I would say that this is a technical difference between UB and other kinds of API contraints.

From a formal methods perspective, "UB is what the compiler knows about" translates into "UB is baked into the very definition of the language semantics itself". That also makes it different than other API constraints which only locally affect that particular API -- UB literally affects all code. If your language is defined operationally and comes e.g. with a reference interpreter for a "specification machine"/"VM" that is used to define program behavior, then UB must be defined that way as well. It is for this reason that I cannot just propose to use the RustBelt model of borrowing and lifetimes as the definition for aliasing-related UB in Rust -- that's not an operational model. It will (likely) never be immediate UB to use raw pointer to have two aliasing mutable references to a ZST, but we will still consider that illegal code.

Of course, "UB is what the compiler knows about" doesn't tell us (during language design) which API violations we should make UB and which "just" funny logic errors like a misbehaving BTreeMap, and maybe that's what you are referring to. The delineation between UB and other constraints is ultimately arbitrary, but once the choice is made, there is a qualitative, technical difference.

8 Likes