In the presence of reference-counted mutable objects, destructors no longer guarantee that cleanup will happen. But that much is okay. This is a liveness property, and, as far as I can tell, nobody really knows of any non-annoying way to enforce liveness properties with types. On the other hand, “cleanup is the last operation that can be performed on an object” is a safety property, and types are excellent tools for verifying properties of this kind.