Allocator-aware @safe reference counting is still not possible

[jmh530]

On Monday, 30 January 2023 at 22:28:56 UTC, Paul Backus wrote:
> On Monday, 30 January 2023 at 21:54:44 UTC, Richard (Rikki) 
> Andrew Cattermole wrote:
>> On 31/01/2023 10:34 AM, Paul Backus wrote:
>>> So, what, we should allow @safe data structures to call 
>>> @system allocators and simply *assume* that the allocator 
>>> implementation won't do anything weird? And if someone writes 
>>> their own allocator implementation, and doesn't manually 
>>> check that their @system code provides the guarantees that 
>>> the data structures expect, we're ok with them getting memory 
>>> corruption in @safe code?
>>
>> If you can show me papers where mechanical checking of memory 
>> allocators take place without the use of proofing assistants, 
>> I'll be very interested in it.
>
> Once again, it seems that I have utterly failed to communicate 
> the fundamental premise of this discussion. This has nothing to 
> do with verifying the allocator's implementation (which I agree 
> must be done by hand).
>
> [snip]

But spelling it out in more detail will help for any future DIP.

I think part of the problem is the whole "can't prove a negative" 
of this. Or rather, being able to show that this is the smallest 
language change to enable @safe allocator-aware reference 
counting.

I was watching Walter's Q&A from the recent Dconf and one point 
he makes it that things are much easier for him to understand 
with code examples. Probably goes for others as well. I think 
being able to show simple versions of various attempts at @safe 
allocator-aware RC approaches that either don't work or are 
awkward to use might go a long way to convincing people.