> 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 resu

> 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.