Clean Code Is Not Enough

So much effort is expended on making code look fine at the micro-level: indentation, naming, method size, etc. So little attention is paid to the macro-level: How does everything come together to effect the desired result? Why is it there?

Developers world-wide waste countless hours debugging, not because of anything they have done, but instead because of library authors’ failure to express preconditions, effects, and expected uses. You can’t do anything to guard against this save choose libraries carefully. And all too often you have no choice.

Literate programming tried to address whole-program understanding. Its core idea: Construct a program via a linear narrative that proceeds by progressive refinement to elaborate the entire program. Code chunks can be incorporated by reference into other chunks. The source code is written for human consumption, not machine. The input to the compiler is ultimately produced by weaving chunks together. For a small example of the pretty-printed human-oriented product, see Shane Celis’ Minimal Emacsy Example Program.

But literate programming fizzled. The highest level of documentation you’ll find in many projects today is class-level. That’s not enough to fully comprehend, never mind maintain, a system. Post-hoc analyzers that visualize the rat’s nest of dependencies serve only as adjuvants in sussing out the Escher’s rat’s nest we’ve crafted ourselves.

In the hands of a capable author, a literate program explains the wherefores of the code to its recipients. As test-driven development guarantees all developed code can be tested, literate programming guarantees all developed code can be coherently explained from start to finish.

But that doesn’t mean the code is correct. And that doesn’t mean the code has been coherently specified. Humans are very limited in their ability to cross-check the validity of a complex, interconnected web of logical statements.

This is where specification languages, like Z (pronounced “zed” in this context), come into play. Alloy applies model-checking in a limited universe to the specification. But bridging the gap between specification and implementation remains in the hands of human – all too human! – implementors.

So we come to the notion of extracting programs from a verified proof. If you go at it right, you only arrive at a proof that everything does what you specified it does by way of producing an existence proof. The proof demonstrates by example that your claim, that your app does the umpteen things you say it does, must be true. Once proven, you can extract this latent program, and, ideally, run it.

But let us set aside the opium pipe. We’ve come full circle: Unless all the libraries and all the frameworks you are using in developing your program have been developed in such a way that you can incorporate their specifications directly (and what world would that happen in?), or at least documented such that you can make meaningful and tractable claims you can adopt as axioms, you’ll still find yourself falling through the sandcastles that are all we have to use as the latest app’s foundation.

We can’t, any solitary one of us, fix this alone. Until everyone starts taking responsibility for building their programs correct from the get-go and documenting them so they can be used in line with the assumptions inherent in the built product, we will all continue to suffer from our continued haze of confusion, no matter how sparkling clean and transcendently clear our own code might be.