Is anyone surprised that unsafeInterleaveST can be used to break semantics? That’s why it’s called unsafe… But certainly some uses of it are ok, and we are back to the original question of how to prove that that’s the case (or even what exactly “that” means).