@tomjaguarpaw, having the `SMT`

monad gets in the way of reasoning and writing a clear denotation to code that calls the `solve`

function. With a monad in there I’m now forced to pick an execution order. Testing becomes much more difficult too, because now my properties would have to be monadic.

Even if we end up going that way on our implementation, there is still the question of having a canonical, concrete answer to the question of when is `unsafePerformIO`

safe.

@jaror while I agree that in spoken language the docs are descriptive, its far from letting me know what does that statement really mean. For instance, here’s the `solve`

function I was able to conjure from my experiments (consider `Env`

and `Query`

to be opaque types)

```
{-# NOINLINE solve #-}
solve :: Env -> Query -> Bool
solve gamma = unsafePerformIO $ do
solver <- cvc4_ALL_SUPPORTED True
declareVariables gamma
mv <- evaluate solver >>= newMVar
return $ \ q -> unsafePerformIO $ do
withMVar mv $ \safeSolver -> do
runSolverWith safeSolver $ do
solverPush
assert q
res <- checkSat
solverPop
return $ case res of
SimpleSMT.Unsat -> False
_ -> True
```

I find it quite elegant that partial application embodies sharing the SMT environment. Yet, how do I know I didn’t miss any case? Is the `evaluate solver`

really necessary? I found this e-mail in the mailing list archives that goes in the direction I’m looking for: Prevent optimization from tempering with unsafePerformIO

In a sequential setting, I guess we can say that `unsafePerformIO k`

is safe iff `let x = unsafePerformIO k in (x, x)`

is equal to `(unsafePerformIO k, unsafePerformIO k)`

, where we’d have some leeway on what “equal” means. do you know of a set of such “equalities” that could help provide a more formal footing to “performs no side-effects” and “independent of its environment”?