To be a better programmer, write little proofs in your head
Home
About
-->
Sign in -->
Subscribe -->
This is a brief write-up of a trick I learned that helps me write code faster and more accurately. I say "trick", but it's really something I started to do without noticing as I moved further into my career.<br>When you're working on something difficult, sketch a proof in your head as you go that your code will actually do what you want it to do. A simple idea, but easier said than done: doing this "online" without interrupting your flow takes a lot of practice. But once you get really good at it, you'll find that a surprising amount of the time your code will work on the first or second try. It feels a little magical.<br>There are lots of ways to pull this off, and I don't want to be too prescriptive. I'll just list a few examples of the kinds of things I find myself reasoning about on the fly, so you get the general idea.<br>Monotonicity<br>Something to keep an eye out for when proving things to yourself about your code is which parts are monotonic.<br>You're probably familiar with monotonic functions from mathematics. Informally, they're functions that don't "go backwards" - i.e. an increasing monotonic function can only increase or stay the same, while a decreasing monotonic function can only decrease or stay the same (these are also known as nondecreasing and nonincreasing functions, respectively.)<br>The concept of monotonic code is a little more nebulous than the concept of a monotonic function, but it captures the same idea of a process that can only proceed in one direction. Check-pointing, for example, is a great example of monotonicity. If you have (say) a script that needs to perform multiple tasks in sequence, you can keep a bit of state around on disk that details how many tasks you have completed so far. If something goes wrong and your script crashes, it can check the on-disk state to figure out how far it got, then start again from the earliest state that hasn't been run yet.<br>Checkpointing means that the "current step" pointer in your script can only go forwards, since the script can't regress and re-run a step it's already done. In this sense the script progresses monotonically, and it's apparent that if the script ever completes successfully, it will have run every step exactly once.
Keeping this kind of activity log is a simple idea that often pops up in surprising places, such as journaling file systems and database write-ahead logs. Another, more involved database example is an LSM tree. LSM trees are used in some databases to store rows in-memory and on-disk, and most of the time they are purely additive. Put loosely - an LSM tree keeps a log of all inserts, deletes, and updates, and scans the log to reconstruct the appropriate value of the row when the row is read. Stale operations are periodically discarded to save space in a process called compaction. The space taken by an LSM tree only grows (except during compaction, when it only shrinks.)
You can compare this to a B-tree, which is a more traditional database structure that deletes and updates rows in place. B-trees generally have to do a lot more work to reclaim the freed space after a delete, restructure things so there's room if an update grows a row, make sure there's enough buffer, etc. If you want, read a little bit more about B-trees and LSM trees, and see which one feels more intuitive to reason about.
It's worth keeping an eye out for monotonicity, because you can usually use it to rule out wide swaths of possible outcomes. Another variation on this theme is immutability (which in a lot of ways is monotonicity's cousin) - when you create an immutable object, that object cannot be modified. Values can be assigned to an immutable object exactly once, at the time of the object's construction; you can't "back out" or "undo" the assignments. This allows you to ignore, out of hand, all scenarios in which an object might change out from under your feet.<br>Pre- and post-conditions<br>Pre-conditions and post-conditions are ways to specify constraints on the behavior of a function. A function's pre-conditions are the things that are assumed to be true just before the function runs. These can be conditions on the function's input, or more general claims about the program's state or environment. A function's post-conditions are things that are assumed to be true just after the function returns. As with pre-conditions, these claims can involve just about anything. If the pre-conditions of a function are true before the function runs, and the post-conditions are not true after the function finishes, then the function is not implemented correctly, at least according to the specified constraints.<br>These are simple (even obvious) concepts and not really proof techniques in and of themselves, but simply keeping track of what they are in formal terms can aid your reasoning.<br>(Sometimes you may come to find that your function does not have well-defined...