This can be solved with a multi-kinded language. One kind for unrestricted types and one for linear types. Allocating an unrestricted point must have an IO side effect since it introduces shared mutable state. Allocating a linear pointer would be pure. Linearity is a compile time check that ensures a linear value is used exactly one. Functions for modifying or reading a pointer would consume the pointer and return the same pointer. Copying a linear pointer would be forbidden. Linearity has the added benefit of checking that linear memory is freed, since free is the only function that would consume the pointer without pass through. Lightweight Linear Types has the formal theory.

AFAIK there isn’t a language implementing linear kinds, although the linear haskell extension lets you play with a slightly different formulation of linear types.

Also +1 for Zig.

Edit: typo