I think if your code does use references in a way that does not let you guarantee memory safety without an extremely convoluted type system, you should perhaps

I think if your code does use references in a way that does not let you guarantee memory safety without an extremely convoluted type system, you should perhaps just be using GC. For most code I personally know, that does not play well with GC (firmware, hard real-time, etc.), you really don't want to do much allocation after initialization anyway, and the little you do can be handled by malloc/free style manual memory management, or perhaps by escape analysis. And then I think Nimrods approach might work well, because you could declare that everything done by a proc should be verified by escape analysis, rather than manually tagging each pointer used in that procedure. But I recognize that Rusts approach should be extremely useful in a few applications. But then again I wonder if Nimrods type-system eventually will be able to implement its most useful pointer types in a library.