|
|
|
|
|
by trealira
951 days ago
|
|
> 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. |
|