Think Above (before) the code

[sanjarcode]

Video and the slides used.

Premise: Before doing an action, one must think. And thinking cannot be done without 'writing'. Thinking before coding is just the action of writing abstract/mathematical specs.

Leslie demonstrates the power of writing specs, and the disadvantage of not doing so, by coming up with a non-recursive, core-agnostic (i.e. multicore, single core processor) algorithm for quick sort. Normally, people are unable to come up with this, because their 'minds are stuck in the code', instead of thinking mathematically.

He says that one must think in the language of mathematics before writing code, and that thinking means writing specifications (specs). The disadvantage of not doing so is the existence of a lack of thinking ability to come up with architecture-agnostic algorithms, and thinking being stuck to a particular architecture.

[sanjarcode]

He tells that even if one does not need or wish to write specs, learning to write formal specs will develop the capability to think mathematically about algorithms/programming, which is essential, in the long run.

[sanjarcode]

He is using a language called TLA+. This may not be the best language, but one should learn and be comfortable in writing formal specs.

[sanjarcode]

Empirically/experimentally, writing specs has helped:

1. Teams at Amazon on complex projects
2. Discovered a flaw in Xbox's memory system, which would go undetected with the current testing systems.

So instead of 'formal spec will slow down progress', formal specs have sped up and served as a correction guarantee for real-world systems too. This is a very important observation.

[sanjarcode]

My opinion: I always want/wish to first construct a mathematical model/system before implementing code. This should be abstract and agnostic to the implementation environment.

So, my goal is to learn what Leslie demonstrated, i.e. writing specs.

Moreover, I always lacked some language/writing structure before doing Data Structure and Algorithm problems. I feel this is the solution for it - formal specs.

[sanjarcode]

This is hard to do, because thinking is hard.

[sanjarcode]

Note that 95% of programming does not require formal specs. But the remaining 5% can screw up the system.

[sanjarcode]

TDD (Test Driver Development) uses examples, not specs (normally). So specs should be written even if TDD is being used. TDD verifies - nothing is wrong, but not - everything is right.

[sanjarcode]

Coding is still a requirement. Spec catches algorithm errors, not program errors.