> That's an extremely narrow view which you wouldn't have if you ever tried to implement a safe sandboxed environment. That is, an environment without effects?

> That's an extremely narrow view which you wouldn't have if you ever tried to implement a safe sandboxed environment. That is, an environment without effects? In Haskell you could't do so, since pure functions allocate, throw exceptions, trigger GC etc. > have you heard about referential transparency? It's the thing your "theorem prover" example does not have. Of course it's. conj "A" "B" can be safely replaced by "A /\ B"