They are declarative vs imperative and sufficiently smart tooling exists such that they can be checked and enforced statically, see liquid haskell and "refineme

They are declarative vs imperative and sufficiently smart tooling exists such that they can be checked and enforced statically, see liquid haskell and "refinement" typing for an example. Formal verification starts to become a possibility -- enforcing both conformance and documentation. Tests are fine too but more tedious work.