21st Century Proof :: Structure makes it possible, hard work makes it probable
- A new way of expressing: “work smarter not harder” -> Structure makes it possible, hard work makes it probable.
- Detail can obscure the big picture. Structure can help, if it allows for a personalized, or tunable about of illumination.
- A proof is not easy if we must read the entire proof to understand.
This weekend I skimmed Leslie Lamport’s How to Write a 21st Century Proof. In it Lamport discusses how mathematicians process for proof has largely unchanged since the 17th century, “…Newton’s Principia seem quite modern…” he states. While I don’t aspire to proof, this paper provides two illuminating points I want reflect. One more philosophical regarding the nature of working smart and working hard. The second, how structure itself is worthy of praise.
A better work smarter
My issue with the platitude, “…work smarter not harder…” is that much of the work I do is hard. Applying intelligence, rigor, or discipline doesn’t not, in general, nullify hard work. Lamport’s recasting is insightful. It’s that because our work is hard, doing it without “smarter” approaches renders it impossible.
Structure makes is possible, hard work makes it probable.
For the task at hand, proof writing, structure provides a clarity that small details aren’t missed. Its the “work smarter” component of the process. Only after this is a good result possible. Only after this does the real work begin.
Structure is work, good work.
In my daily work, “working code speaks loudest”. The key operational word here is working. Working code speaks loudest. I feel the stress on working is too often lacking. This phrase is used to assert that we should just start coding to show or prove1 that something is a good idea. I understand the concept of play. Playing with code/idioms/tools to see if something is possible. However, to have a consistently good, consistently working outcome, it takes structure.
Lamport, here, discusses structure in terms of a proof. I have a phrase, ’turn the crank’. In it I mean, reduce the hard things to a process so you can just turn the crank to crank out the next thing, or the incrementally better thing. A lack of structure and/or process doesn’t necessarily allow one to crank. Instead it leaves each successive step with this dilemma of what direction analysis paralysis. A structure around the problem at hand, allows one to continuously cut the problem in half. Each decision cuts off a branch of work one doesn’t need to do, or is not important at the moment. The last of structure leaves one without this narrowing of effort.
I enjoyed the paper, and it’s filled with interesting exercises to the reader around proof, and building structure. I’m choosing to ignore these for now, and focus on model checking as I work on a new project idea called “Riffing Algorithms”.
Prove in the colloquial sense, not the rigorous. mathematical sense. ↩︎