Tue Dec 27 12:42:52 EST 2016

types vs. tests

Translations and communication: usually types are sufficient for this,
as the functionality is mostly implemented by composing obvious
sub-solutions into an obvious solution, where the complexity is just
in getting it not to do undefined things.

Algorithms: types are not sufficient, as algorithic steps usually
contain "cleverness" in a way that can not be expressed easily through
type systems.  Custom properties are often at play that cannot be
expressed in the implementation language. In that case there are a
couple of options:

- manual proofs
- a model in a different language with more checkable/provable properties
- property based testing
- manual testing