Abstract: Lehman’s Laws distinguish between stable S-type and volatile E-type code. Developers can decompose unique problems methodically by seeking standard sub-problems, which reduces complexity and boosts productivity. This illuminates the nature of software engineering, which is needed whether code is written by humans or machines.
The overall idea of using your type system to enforce invariants is called typeful programming [1]. The first few sentences of that paper are:
"There exists an identifiable programming style based on the widespread use of type information handled through mechanical typechecking techniques. This typeful programming style is in a sense independent of the language it is embedded in; it adapts equally well to functional, imperative, object-oriented, and algebraic programming, and it is not incompatible with relational and concurrent programming."