| Personally, I don't see the issue. We are including arbitrary C code. For this to be safe, there are additional proof obligations. The function `unsafePerformIO` is the same - for it to be safe, additional proof obligations have to be met. Concerning a `runST`-like device, if the idea is to limit the scope of effects that are permitted by putting it into another monad and using a different interface, then this will at least complicate the API quite considerably. Currently, marshalling is performed by functions that read and write arbitrary memory locations. The FFI needs these functions anyway; hence, any other marshalling would need to add functions in addition to the existing ones. Secondly, marshalling is somewhat unpredictable in that different C libraries require different marshalling. Providing an interface with limited effects that captures all possible situations seems tricky, but if anybody has a concrete proposal, let's see it.