Wow, thanks for that. I have been hacking creating a novel memory reclamation scheme for Go and somehow I missed that. It is similar to something I have implemented but DLG has yhe model for a TLA proof and it might indicate a possible improvement that I wasn't making.