> Bacon/Dingle tell us that a correct Gel-program doesn't need a refcounted GC > at all. To check this, they still have the refcount and offer us a runtime > error (?!). That's odd.
Nothing odd about it -- otherwise you end up with either memory unsafety for doubly linked lists (Rust) or with a type/proof system that uses "separation logic" which not even Z3 supports ( [https://github.com/Z3Prover/z3/issues/811](https://github.com/Z3Prover/z3/issues/811) ).
