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

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

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

Knuth: It turned out that the inventors of the GNU debugger realized that you could have preprocessors writing programs. So you can correlate the low-level stuff to a high-level source in a completely different language. So I’m writing in CWEB but I still never have to look at the lower-level things because 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 binary instruction but GDB knows that this came from something in my WEB source file even though WEB came 10, 20 years after C. So it was a very good, 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 might slow the whole thing down by a factor of 100 if I turn it on.

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

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

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

I’ll also write something that gives a nice symbolic form of a data structure so 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 can dump it out in a file and I can write another program that analyzes it to find out what’s going wrong.

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

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

The very first paper by Tony Hoare about formal proof, “Proof of a Program: 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 them that 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 than anybody else had at that point.

Now, the program that I did yesterday—I have no idea how I would state all of the assertions that are there. I would never get done because I wouldn’t have 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 correct would be incomprehensible. Some methods for formal semantics are so complicated that nobody can comprehend the definition of correctness.

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

Knuth: Right.

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

Knuth: Well, I’ve been a nitpicker all my life. So if I can get my kicks out of finding errors then I just have to make sure that I forget that I was the author 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 know why.

For example, some of the best work I did for Burroughs Corporation was to debug their hardware designs. Their engineers would show me the specs for their computer and I would look at it and I would try to construct examples where they would be off by 1 or something. I got more than 200 bugs 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 correct according to the semantics of the language but the machine would then execute incorrectly?

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

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

Knuth: Am I just a mean guy? I don’t know. But if I’m trying to prove something—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 get psyched up to find a hole in this or explain why it doesn’t work. And then when 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. My juices are working when I’m playing the game as the opponent rather than if I’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 is explaining things. Do you think that approach somehow feeds into how you explain things?

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