I have some qualms with the design, specifically the fact that it seems to ignore data races, but... > Wouldn't the safe way to write that code be to just allo

I have some qualms with the design, specifically the fact that it seems to ignore data races, but... > Wouldn't the safe way to write that code be to just allocate the value on the stack so it has automatic lifetime managed for you? To be fair, there are a lot of reasons why you might not do that. One reason is that stack space is limited, so if you are allocating a large object, it would be unwise to necessarily use stack space in some cases, as you might overflow the stack, and it's hard to know if your code is overflow-prone since different platforms have different default max stack sizes. Another reason is if you don't know how much memory you might need at compile-time and thus can't use static allocations. Finally, and probably one of the main reasons, sometimes the lifetime of a memory allocation just doesn't map to a stack frame; it may malloc/free within one stack frame, or it may malloc and then get freed in a parent stack frame indeterminately. Basically, any reason you might use a smart pointer in C++ is also a reason you'd reach for dynamic allocations in C. Sure, if you malloc(1) specifically, you know it's only one byte, and a static allocation. But clearly, that's just a contrived example, so focusing too hard on it is a little silly. > Excepting that, why are you annotating functions, it's the pointer itself that has the use case invariant. Shouldn't the type be annotated to declare these semantics instead? Their entire hypothesis is the idea that the boundaries between interfaces is where the unsafety occurs. The pointer itself has the invariant, but locally proving invariants like "pointer can never be freed twice" or "pointer is either freed or returned" can be done trivially using control flow analysis; the problem comes when you start calling other functions. If you add annotations and make it a compiler error to have invalid annotations, you can make it so that these invariants can extend across function boundaries without needing to recursively prove the control flow over the entire program, which would usually be infeasible due to the amount of possible code paths. I'm not suggesting this is necessarily the best way to go FWIW, but this is also pretty similar to how, say, TypeScript adds incremental safety to JavaScript; null safety is accomplished by having not just the types but also the interface boundaries contain assertions that can be checked on both sides to avoid needing deep, recursive control flow analysis.