[timschmidt]

Second, less-predictable execution path. Additional cognitive load in evaluating effects across both paths. Additional opportunity for bugs. Doesn't necessarily mean that exceptions make all software which uses them unsafe, but does tend to mean that exceptions significantly complicate the task of proving safety for any nontrivial program.

[trealira]

> proving safety for any nontrivial program.

I haven't done this, but probably the surest way to do that would be to use a proof assistant and extract the result to Standard ML or to OCaml. Standard ML has verified implementations, too.