“Peyton Jones: Sometimes to say that it's obviously right doesn't mean that you can see that it's right without any mental scaffolding. It may be that you need to be told an insight to figure out why it's right. If you look at the code for an AVL tree, if you didn't know what it was trying to achieve, you really wouldn't have a clue why those rotations were taking place. But once you know the invariant that it's maintaining, you can see, ah, if we maintain that invariant then we'll get log lookup time. And then you look at each line of code and you say, “Ah, yes, it maintains the invariant.” So the invariant is the thing that gave you the insight to say, “Oh, it's obviously right.” I agree completely that just looking at the bare code may not be enough. And it's not a characteristic, I think, of beautiful code, that you should be able to just look at the bare code and see why it's right. You may need to be told why. But after you have that, now with that viewpoint, that invariant, that understanding of what's going on, you can see, oh yeah, that's right.”