Peter Seibel - Coders at Work - Reflections on the craft of programming

Seibel:That seems to be a common story. It sort of makes you wonder about the utility of writing better debuggers if so many people get by with print statement debugging.

Peyton Jones:There’s a cultural thing though. On the .NET platform with debuggers that people have put tens or hundreds of man-years into engineering, I think it’s a qualitatively different experience. I think debuggers do require perhaps more engineering cycles to get to work well. But if you put them in, you do get something that is really quite remarkably more helpful.

Maybe the people that you’ve been mainly talking to are more in the academic software mold. And also perhaps have grown up with sophisticated debugging environments less. I wouldn’t like to draw any general lessons. I certainly wouldn’t wish to denigrate or downplay the importance of good debugging environments. Particularly in these rather complicated ecosystems where there are many, many, many layers of software. GHC is a very simple system compared to a full-on .NET environment with layers of DOMs and UMLs and I don’t know what kind of goop. The real world gets so goopy that more mechanical support may well be really important.

Seibel:Another approach to getting correct software is to use formal proofs. What do you think about the prospect of that being useful?

Peyton Jones:Suppose you declare that your goal is for everything to have a machine-checked proof of correctness. It’s not even obvious what that would mean. Mechanically proved against what? Against some specification. Well how do you write the specification? This is now meant to be a specification of everything the program does. Otherwise you wouldn’t have proved that it does everything that it should do. So you must have a formal specification for everything it should do. Well now—how are you going to write that specification? You’ll probably write it in a functional language. In which case, maybe that’s your program.

I’m being a bit fast and loose here because you can say some things in specification languages that you can’t say in programs like, “The result of the function is that y such that y squared equals x .” That’s a good specification for a square-root function but it’s not very executable. Nevertheless, I think to try to specify all that a program should do, you get specifications that are themselves so complicated that you’re no longer confident that they say what you intended.

I think much more productive for real life is to write down some properties that you’d like the program to have. You’d like to say, “This valve should never be shut at the same time as that valve. This tree should always be balanced. This function should always return a result that’s bigger than zero.” These are all little partial specifications. They’re not complete specifications. They’re just things that you would like to be true.

How do you write those down? Well, functional languages are rather good at that. In fact this is exactly what happens when you write a QuickCheck specification; you write down properties as Haskell functions. Say we want to check that reverseis its own inverse—well, you might write checkreversewith type list of A to bool. So checkreverseof xsis reverseof reverse xsequals xs.So this is a function that should always return true. That’s what a property function is. But it’s just written in the same language—so that’s nice.

Now you might hope to do some static checking on this. It might be hard or easy. But even having the property written down in a formal way is a real help. You can test it by generating test data, which is, indeed, just what QuickCheck does.

So rather than trying to write down specifications for all that a program does I think it’s much more productive to write down partial specifications. Perhaps multiple partial specifications. And then check them either by testing or by dynamic checks or by static checks. You never prove that your program is right. You just increase your confidence that it’s right. And I think that’s all that anybody ever does.

Seibel:So you define however many properties, covering the things you care about. And then you can choose to confirm that those properties actually hold either statically or dynamically, depending on what’s actually feasible. Because we may not know how to statically check them all?

Peyton Jones:Right. But in a functional setting, you have a better chance. But we’ve still been dragging our feet a bit about demonstrating that. Nevertheless—step one is to write down these properties in the first place.

But I think the big thing is to get away from this monolithic, all-or-nothing story about specification and to say that you can do useful static and dynamic tests on partial specifications. These will increase your confidence in the correctness of your program and that is all you can possibly hope for.

Even the allegedly complete specifications miss out—you know, it has to work in .1 of a second. Or must fit in 10KB of memory. Resource things are often not covered. Or timing things. There’s endless little stuff that means the program might actually not function as desired even though it meets its formal specification. So I think we’re kidding ourselves to say we’ve actually proved the whole thing is completely right. Best thing to do is to acknowledge that and say we’re improving our confidence—that’s what we’re doing. And that can start quite modestly—you might have improved your confidence by 75 percent with only 5 percent of the effort. That’d be good.

Seibel:Let’s talk about concurrency a little bit. Guy Steele asked me to ask you: “Is STM going to save the world?”

Peyton Jones:Oh, no. STM is not going to save the world on its own. Concurrency, and parallel programming generally, is a many-faceted beast and I don’t think it will be slain by a single bullet. I’m a diversifist when it comes to concurrency.

It’s tempting to say, “Use one programming paradigm for writing concurrent programs and implement it really well and that’s it;” people should just learn how to write concurrent programs using that paradigm. But I just don’t believe it. I think for some styles of programming you might want to use message passing. For others you might want to use STM. For others data parallelism is much better. The programmer is going to need to grapple with more than one way to do it.

But if you ask me, is STM better than locks and condition variables? Now you’re comparing like with like. Yes. I think it completely dominates locks and condition variables. So just forget locks and condition variables. For multiple program counters, multiple threads, diddling on shared memory on a shared-memory multicore: STM. But is that the only way to write concurrent programs? Absolutely not.

Seibel:A criticism I’ve heard of STM was that when it really gets down to it, optimistic concurrency won’t allow as much concurrency as you hope. I think the claim was you can fairly easily get in these situations where you’re really not making progress.

Peyton Jones:You do have to worry about starvation. My favorite example here is of one big transaction that keeps failing to commit because a little transaction gets in there and commits first. So an example would be a librarian who’s reorganizing their library. They start optimistically reorganizing their library. And they’ve got two-thirds of the way through and an undergraduate comes along and borrows a book. Well, he commits his transaction successfully because the library reorganization hasn’t committed. The librarian gets to the end and discovers, ah, I saw an inconsistent view of memory because the library changed while I was reorganizing it so I just have to go back and start again.