Incremental Development

The point of programming techniques and methodologies is to reduce cognitive load, not to increase it with additional seemingly related concepts or tricks. We, humans, have very limited mental capacity so care should be taken not to overwhelm ourselves and others with unnecessary, redundant abstractions or irrelevant details.

Things like modules and namespaces, when done right (small functions, small modules) tend to partition the problem domain into manageable pieces (building blocks) along with conceptual boundaries to make unrelated concepts decoupled from each other and to share nothing.

With Algebraic Data Types (and Abstract Data Types in general) one doesn’t have to write everything down at once. Write what you have already figured out, what you know so far.

Partially specified concepts will do. They reflect one’s partial knowledge due to imperfect information or simply not being able to figure everything out as a whole yet.

With a sum-type each new variant could be added and tested separately and independently (by explicit pattern-matching).

Same goes for records (named or indexed product-types) as long as one is accessing by a name or a “key” (get by getters and set by setters, which is how one uses an Abstract Data Types in principle).

This, by the way, is why SELECT * FORM blah is lame - one simply throws everything that is principle-guided out of the window.

Just like in mathematics, in a pure-functional programming once you have figured it out and wrote down right (no type-errors and all tests passed) it becomes “eternal” - correct and valid.

Gregor Kiczales

Gregor Kiczales has a whole course about Systematic Program Design on youtube (based on his MOOC). Just watch it, even if it a bit too pedantic (which is actually good).

Really, this is one of the best and highest quality courses out there.

Write the type-signatures first

It should be one’s habit to write a prototype of the module-signature (.mli in Ocaml) first. You will at once “see” how consistent and uniform your naming and parameters are (the same order).

I wish every language would have a support of Ocaml modules (sigs, structs and functors). They are absolutely brilliant. This is what Haskell lacks.

Second step - write a test-case

Write a failing test case first and then implement the function to make the test pass. This is the crucial pont of whole TTD approach.

Writing tests before the implementation allows on to focus on the interface (function signature) and the call-site, which are much more important considerations.

If a function has already known preconditions write test-cases which explicitly specify them and catch the proper exceptions or fatal errors (failed assetions).

REPL

A REPL is the tools of experimentation and rapid prototyping due to instant feedback and real quick setup (because pure functions share nothing and could be applied without setting of a context, in any order).

In a REPL you try the things to feel the “use-side” (the call-site).

Tests as crude pseudo-specs

Writing down specifications for interfaces (for every exported function) is crucial, but instead of writing them in commentaries, write them in unit tests, even before the implementation is figured out.

Thus we will create poor man’s executable specifications. Well, sort of.

do defensive programming and always assert /preconditions.
specify and test the invariants first (with assertions and logic)
\(\forall\) and can be emulated with explicit “corner cases” and a quickcheck generator
\(\exists\) is just a search, which may require a presorted copy.

Remember that tests will never show the absence of bugs, but will show their presence early.

Formal specification

The critical functions can be fully specified and veryfied using advanced tools, like TLA+, Coq or Agda.

This is, basically, just to write down all the underlying math explicitly.

It is also possible to bottom-up bootstrap a function in Coq and then export it in Haskell (automatically) or any other functional language (manually).