Memory/Allocation attributes for variables

[Ola Fosheim Grøstad]

On Monday, 31 May 2021 at 18:21:26 UTC, Elmar wrote:
> I wonder how programming languages don't see the obvious, to 
> consider memory safety as a part of type safety 
> (address/allocation properties to be type properties) and that 
> memory unsafe code only means an incomplete type system.

All high level programming-languages do. Only the low level 
don't, and that is one of the things what makes their type 
systems unsound.

> constraints. Memory safety is violated by storing a pointer 
> value in a reference which is out of the intended/reasonable 
> value domain of the pointer (not matching its lifetime).

But how do you keep track of it without requiring that all graphs 
are acyclic? No back pointers is too constraining.

And no, Rust does not solve this. Reference counting does not 
solve this. How do you prove that a graph remains fully connected 
when you change one pointer?

> One important aspect which I forgot: aliasing of variables. I 
> know, D allows aliased references as arguments by default. Many 
> memory safety problems derive from aliased variables which were 
> not assumed to be aliased.

So, how do you know that you don't have aliasing when you provide 
pointers to two graphs? How do you prove that none of the nodes 
in the graph are shared?