What's the go with the GC these days?

[Ola Fosheim Grøstad]

On Monday, 7 January 2019 at 02:00:05 UTC, H. S. Teoh wrote:
> Just out of curiosity, any concrete examples of difficulties 
> that prevent easy elision of counter bumps?

Let's say you obtain ownership of every other object in an array, 
then you have to prove that  you also release every other object 
in that array before you return from the function.

If you always hold onto the ref-counted object in a named 
reference that is never changed, then it is reasonably easy to 
do. Then you only have to prove that the acquired object is 
released once while the reference is live.

So basically, whenever the recounted object is accessed through a 
graph-like structure then you need an advanced prover.