> with a type/proof system that uses "separation logic" which not even Z3 > supports
Well, the `[``adapt: ]` can't be inferred by the compiler generally. `[``adapt: ]` is annotated by the API programmer and tells the compiler, that the proc behaves _like a template_ and can be seen as part of the scope of the calling proc. But contrary to a template, the annotated proc might call other procs that obey the same (or derivable) annotations. (Don't try the templates, they will lead you into a dead end...) > No, it's a runtime check not unlike array bounds checking is, you don't get > speed from it. I had a pool allocator in mind, where the allocator draws memspace from a list of memory regions and the refcount bookkeeps the refs (summarized) _into_ entire regions. When such a refcount becomes zero, then the entire memory region will get freed and therefore, you will get _some_ speed. > If you use the counters to delay the deallocations the system is the same as > atomic reference counting with all its known downsides. If you deallocated successfully thousands of nodes (list elements respectivelly) and a couple of them remain as "temporarily not deallocatable" , then you certainly will keep the advantages of Bacon/Dingle if there are some. The primary problem of Bacon/Dingle are the abundant refcount updates coming from local refs on the stack. Something that the recent GC avoids. Deterministic deallocation is not making Bacon/Dingle automatically a better design.
