Reasoning about correctness in Standard ML is easier than in either Haskell or OCaml, since induction on strictly positive datatypes actually works as a reasoni

Reasoning about correctness in Standard ML is easier than in either Haskell or OCaml, since induction on strictly positive datatypes actually works as a reasoning principle. You don't need to manually assert silly preconditions such as “this list is finite” (Haskell) or “this list isn't cyclic” (OCaml). On the other hand, neither Haskell nor the MLs tackle the problem of safely managing ephemeral resources. Rust does this, but it sacrifices the ability to conveniently share immutable data structures (Rc and Arc exist, but they aren't very convenient). The good news is that this doesn't have to be a dichotomy. You can have GC for in-memory data structures and deterministic destruction for everything else: https://news.ycombinator.com/item?id=12766781 https://news.ycombinator.com/item?id=12766781