Seibel: In your earliest days you were writing machine code; then youfound structured programming, which provided literally a structure fororganizing programs. And then you invented literate programming, whichgave you another way to structure programs. Since the invention of literateprogramming, has there been anything else that’s as dramatically changedthe way you think about programming?

Knuth: I’ve got better debugging tools for literate programming; that’sbasically all.

Seibel: OK, let’s talk about debugging. What better tools do you havenow?

Knuth: It turned out that the inventors of the GNU debugger realized thatyou could have preprocessors writing programs. So you can correlate thelow-level stuff to a high-level source in a completely different language. SoI’m writing in CWEB but I still never have to look at the lower-level thingsbecause it’ll flash my CWEB source as I’m stepping through the program.

Seibel: So that’s a facility built into GDB which CWEB takes advantage of?

Knuth: And was built into GDB because it was built into C to have__LINE__ directives. We had to work to make use of the __LINE__directives,but it works beautifully. The computer is sitting there with a binaryinstruction but GDB knows that this came from something in my WEBsource file even though WEB came 10, 20 years after C. So it was a verygood, very forward-looking part of their design to make that work.

Seibel: So you use GDB. What other debugging techniques do you use?

Knuth: I’ll add a lot of code that will check to see if my data structures,with all their redundancies, are properly done. This sanity checking mightslow the whole thing down by a factor of 100 if I turn it on.

For instance, I had a complicated data structure that involves referencecounts. So I’m writing some pretty complicated programs, and getting thesereference counts correct is mystifying. Every once in a while I have toincrease the reference count or decrease the reference count. But when apointer is in a register or is a parameter to a subroutine, does that count asa reference in the data structure or not? So I’ve got the sanity check writtenthat goes through the millions of counts seeing how many references arereally made and are the numbers correct? Then I’ll do a little computationand check the whole thing. That way errors will be detected billions of stepsbefore they would surface in a crash.

There was a program that does multiplication in a new way, so I tried itexhaustively. I made 256 numbers and I multiplied each of them by each otherone, but after each one I would do a sanity check. I multiply 2 by 3—fails! SoI fixed that. And then something else. Finally I got it to where all 256 by 256were working and getting the right answer.

So that’s an important debugging technique for me. Maybe ten percent ofthe code is devoted to something that I don’t need except when I’mdebugging. And the sanity-check code also documents the data structure.

I’ll also write something that gives a nice symbolic form of a data structureso I don’t have to decode a whole bunch of binary things. Then, if necessary,I can print out a data structure in some decent structured form or I candump it out in a file and I can write another program that analyzes it to findout what’s going wrong.

Seibel: Related to invariants and various kinds of assertions, folks likeDijkstra would argue that we’ve got to put very formal assertions at everystep of our program so that we can then prove our programs correct. I’veread where you’ve talked about wanting to prove your programs “informallycorrect”; what’s your take on the idea that we should go beyond that andformally prove things correct?

Knuth: On one hand you have this impossibility of ever having somethingproved. Somebody will say they have a program that’s verified and it’s onlyverified because it met its specifications according to some verifier. But theverifier might have a bug in it. The specifications might have bugs in them. Soyou never know that the program is correct. You have more reason tobelieve it, but you never get to the end of the loop. It’s theoreticallyimpossible.

The very first paper by Tony Hoare about formal proof, “Proof of aProgram: FIND,” was a great achievement and advanced the state of the art.But there were two or three bugs in that proof. It hadn’t occurred to themthat you had to verify that subscripts lie in-bounds or something like this.There’s always a chance for gaps. Still, he had verified it much more thananybody else had at that point.

Now, the program that I did yesterday—I have no idea how I would state allof the assertions that are there. I would never get done because I wouldn’thave any more confidence in my assertions than I would in the program.

Or TeX, for example, is a formal mess. It was intended to be for human use,not for computer use. To define what it means for TeX to be correctwould be incomprehensible. Some methods for formal semantics are socomplicated that nobody can comprehend the definition of correctness.

Seibel: When you were working on TeX you wrote a really horrendoustorture test of the program.

Knuth: Right.

Seibel: How do you get in the frame of mind to do that? Programmersoften tend to want to protect their baby, and so they don’t test as hard asthey could.

Knuth: Well, I’ve been a nitpicker all my life. So if I can get my kicks out offinding errors then I just have to make sure that I forget that I was theauthor of the program. I try to imagine that somebody else was the author.But otherwise it’s fairly easy for me to get into attack mode. I don’t knowwhy.

For example, some of the best work I did for Burroughs Corporation wasto debug their hardware designs. Their engineers would show me the specsfor their computer and I would look at it and I would try to constructexamples where they would be off by 1 or something. I got more than 200bugs out of their B-5000–series machines before they went into production,although it had passed the simulators.

Seibel: So essentially you were inventing programs that were correctaccording to the semantics of the language but the machine would thenexecute incorrectly?

Knuth: Right. Certainly if their floating point isn’t calculating the rightproduct of two numbers, I would try to find examples of numbers wherethe floating point didn’t work. But also there were cases where they wereimplementing a stack in hardware and they had cases where registers wouldbe empty or not at the top of the stack and I would find scenarios wheretheir logic would get screwed up.

Seibel: Did you have a systematic way of doing that? How did you findthem?

Knuth: Am I just a mean guy? I don’t know. But if I’m trying to provesomething—a theorem in mathematics—instead of proving that it’s correct,it’s easier for me, usually, to say, “Well, find a counterexample.” I can getpsyched up to find a hole in this or explain why it doesn’t work. And thenwhen I can’t find any holes, then I see the proof.

I think it’s just my personality that I like to attack things and find errors. Myjuices are working when I’m playing the game as the opponent rather than ifI’m just sitting there trying to say, “Oh, yeah; now why is this working?”

Seibel: It’s curious that that’s what gets you going, yet your life’s work isexplaining things. Do you think that approach somehow feeds into how youexplain things?

Knuth: The only thing I can claim for my explanations is that I try to matcha natural brain process of seeing things in two different ways at a time inorder to understand something better. I think the key is usually to have astereo view instead of a one-dimensional view. I don’t know how thataffects this attacking business.