Linear types and separation logic are both great, but can require quite a bit of programmer effort. Writing a safe linked list in Rust could be pretty hard, for instance.
But there is an alternative that requires much less programmer effort, although with less strict guarantees. A (pretty old) stream of work is to guarantee memory safety by using (usually a stack of) regions. Using region inference, a compiler can statically decide which region a piece of allocated data should go into, and deallocate the region when it goes out of scope.
Region inference is provably safe (can't deallocate reachable memory) and requires minimal programmer interference, but it is not "total" (i.e. it still can leak memory, although definitely much better than "do nothing"), so it's usually combined with GC in practice. The
MLton ML Kit compiler uses regions to eliminate most GC calls, but it still has a GC because it would still leak memory otherwise. According to some of the early pioneers on regions, region inference wasn't actually invented for this purpose (it was for automatic parallelization, I think); but it just turned out it could be used for memory management as well.
For a starting point, I would say go for the paper "Implementation of the Typed Call-by-Value λ-calculus using a Stack of Regions" by Mads Tofte and Jean-Pierre Talpin. For more papers on region inference, look for other papers by M. Tofte and J.-P. Talpin, some of Pierre Jouvelot's work, as well as Greg Morrisett, Mike Hicks, and Dan Grossman's series of papers on Cyclone.