Haskell still doesn't have real referential transparency. It's all a matter of degrees and no language is pure, even Agda or Coq. The concept of IO as a world s

Haskell still doesn't have real referential transparency. It's all a matter of degrees and no language is pure, even Agda or Coq. The concept of IO as a world state you pass around is deeply flawed, especially with multiple cores. You cannot be in control of the world, so you don't really have equational reasoning. At any rate, there can be unsafePerformIOs lurking anywhere. I really think delimited-continuation based algebraic effects are the way to go.