Allocator-aware @safe reference counting is still not possible

[Richard (Rikki) Andrew Cattermole]

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.

My understanding is that the state of the art barely touches upon this 
subject even with proofing assistants, let alone without. I.e. 
https://surface.syr.edu/eecs_techreports/182/

So yes, if the state of the art literally requires proof assistants to 
verify that a memory allocator is doing the right thing at the bare 
minimum, then it absolutely is out of scope of D for the time being. But 
hey, if there is a known good solution here that we can implement, lets 
do that.