Shortest Proof of Elegance

About two months ago I had an extraordinary opportunity to talk to some Great People in the context of creating a computer science program at Reed College.  These days being in a roomful of people in which I am the least experienced, or nearly least, is not a thing that happens to me so very much.

Imagine being in room full of people, each with so many interesting things to say that you feel the whole time that there are just not enough moments to adequately allow everyone to express what they are thinking.  And rather than wanting to talk so much your overwhelming inclination is that it’s so very important that you yield because it is crucial that the person over there be given a chance to speak because that’s how much you want to know what they think.

That’s what my experience was like.  It was simultaneously gripping and frustrating because it was hard to truly finish a thought and yet there was so much more to learn by listening.

There was one thing in particular that I tried to explain and I feel like I didn’t do nearly as good a job as I would have liked and so I’ve stewed on it somewhat and wrote these few words.  It’s about what makes some computer programs elegant.  And why elegance is, in my view anyway, a much more practical thing than you might think.

For me elegance, simplicity, and correctness are inextricably entwingled.  A notion I’ve been recently introduced to is that the best code is the code “shortest proof of correctness”, but what does that even mean?

Well, for one thing it means that code in which you can apply local reasoning to demonstrate correctness is superior to code in which you must appeal to many broader factors about how the code is combined in some larger context to demonstrate the same.

But already I’m ahead of myself, what do we mean by correctness?  In an academic context one might appeal to some formal statement of given conditions and expected results, but the thing is that process is so very artificial.  In some sense creating those statements is actually the hard part of a professional programmer’s work.

So, in a very real way, putting aside any academic aspirations, or great theories, just as a practiced coder trying to do his/her job, the first thing you must do if you want to be successful is to describe what it is you intend to do in some reasonable way, and why that is right.  It doesn’t have to be fancy, but it’s essential.  In Test Driven Development we say “write a test that fails” which is another way of saying “describe some correct behavior that isn’t yet implemented and do so with code in the form of a unit test”, but the essential idea is to describe your intent clearly.  It's essential because the best you can ever hope to do as far as correctness goes is to demonstrate that the code is working as you intended.

It’s funny that I sort of had to re-learn this over the years.  When I first started coding I didn’t even own a computer so I would make my plans in a notebook.  In my sometimes not-so-little books I would describe what I wanted to do, and even code up things in writing and cross them out and so forth.  I had to do this because there was no computer to tempt me to just “bang out the code” and fix it; thinking about the problem was a necessary pre-step.  When my friends asked me how I went about writing programs I always said, “Well, first you make a plan”.

Intent can and should encompass a variety of factors depending on the situation.  Not just a statement of inputs and outputs but perhaps CPU consumption, memory consumption, responsiveness and other essential characteristics of an excellent solution.   And so correctness likewise encompasses all these things.

When I talk about a “short proof of correctness” I usually mean only in the sense that by looking at the intent and the code that you can readily see that it is doing exactly what was intended without long and complicated chains of reasoning.  And hopefully with limited or no appeal to things that are going on elsewhere in the overall system.  The bad proofs read something like “well because that number way over there in this other module can never be bigger than this other number over in this other module then this bad-looking chain of events can’t actually happen and so we don’t ever have a problem.”

Of course, the trouble with relying on those sorts of long proofs is that changes in galaxies far far away can (and do) break anything and everything, everywhere.

So far we’re only talking about reasoning about the code, but in some sense that’s not enough for an engineer.  To make things better in practical ways you want to have tests that actually try the various conditions and force the code to do the right thing -- or else.  This affirmative verification helps to make sure that nothing is inadvertently broken by those that follow and provides evidence that the reasoning was correct in the first instance.

Likewise in good code we sprinkle other verifications, like “asserts” that will cause the code to immediately fail should underlying assumptions be violated.  This is an important part of the process because occurrence of these unexpected situations mean our proofs are no longer valid and some change is necessary to restore a working state.

All of these considerations are of profound practical value, and it’s a rare situation in which the practical desires to be thorough also result in the most elegant designs, which are necessarily the most minimal and the easiest to understand but do the job.  It's even more amazing that these methods tend to get the best overall productivity for an organization, at least in my experience.

Good results begin by understanding your intent, and describing what a great solution looks like.  When you can show, in far fewer words than this blog, that your code does just what you intended, and you have tests to prove it, and safeguards to ensure your proof does not become accidently obsolete, you will have, in my mind, produced a solution that is indeed elegant.

And we all know beautiful code when we see it.

Comments

• Anonymous
  June 07, 2015
  Readers who know me well will understand how extraordinary it is for me to say that I had an overwhelming desire to listen :)

• Anonymous
  June 07, 2015
  Curious as to your thoughts on programming languages like Idris or Agda, or the directions that Haskell seems to be moving in -- not just asserts, but providing as part of the program real proofs of correctness.

• Anonymous
  June 09, 2015
  My primary rule in programming : qbziz.wordpress.com/.../less

• Anonymous
  June 11, 2015
  @csharper:  I think you can accomplish these practices in a language neutral way and the more formal languages frequently have operating environments that are not friendly to practical engineering. The thing is though, many of the precepts -- like side-effect free, minimal capabilities, no globals etc.  Can be done in practice with assorted languages plus something like fxcop to bust you if you break the rules.  Scanning for out-of-bounds practices can often be done on the cheap.