Just an idea about proving that variable graph is isolated. Maybe it could be done same way as out of bound runtime check is done, at runtime. In dev mode each ref variable has a field with thread id, and if that id is different from the current thread id when you touch that variable, the exception will be thrown. In production build this flag is removed, so there will be no slow down or overhead. Also, if in the future someone would came up with a clever idea how to do that check at compile time, this flag could be removed without nobody noticing it.
P.S. I don't know much about compilers so feel free to ignore it if it sounds stupid.
