Hacker News new | ask | show | jobs
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.