ATS claims to support memory safe functional programming without GC. I never used this language, though.
IIRC the idea is that allocating memory or writing something through a pointer returns a magic "cookie" value which certifies that the pointer now points to a block of certain size or data of certain type. This cookie can be bound to a variable like any other value and passed to other code together with the pointer so that the code can know that it's safe to access the pointer.
There are rules - cookies can't be pulled out of thin air or cloned, have to be destroyed during deallocation, etc. All of this is checked during compilation and removed from the final executable.
IIRC the idea is that allocating memory or writing something through a pointer returns a magic "cookie" value which certifies that the pointer now points to a block of certain size or data of certain type. This cookie can be bound to a variable like any other value and passed to other code together with the pointer so that the code can know that it's safe to access the pointer.
There are rules - cookies can't be pulled out of thin air or cloned, have to be destroyed during deallocation, etc. All of this is checked during compilation and removed from the final executable.
http://www.ats-lang.org/