[fsloth]

Sure, it's limited to a subset of all bugs but with a proper typesystem the category of bugs you can remove from code by just encoding the semantics and algebra into the types is quite large.

So if you know how to formulate the problem so it leans heavily on the type system, you can implement something like a binary tree container, and presume it is correct when it compiles.

Following the same parameters bestows rest of the codebase with this robustness.

See for example the ACM article "Ocaml for the masses" by Yaron Minsky of Jane Street for very lucid practical examples https://queue.acm.org/detail.cfm?id=2038036