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

The extreme example of this was when TeX was adapted to Unicode. They had a change file maybe 10 times as long as the master program. In other words, they changed from an 8-bit program to a 16-bit program but instead of going through and redoing my master program, they were so into change files that they just wrote their whole draft of what they called Omega as change files, as a million lines of change files to TeX’s 20,000 lines of code or something. So that’s the extreme.

But now I use change files all the time because I’m writing programs for myself that I’m using writing my book—I’ve got lots of problems that I want to solve and I want to experiment with different versions. Like yesterday I wanted to find out how big a Boolean circuit is for multiplication of n -bit numbers. I have a program that takes any Boolean function and finds out how big its BDD is. So I’ve got a program that takes any Boolean function and computes its BDD.

In my original program you input the truth table of the function online—it says, “Give me a truth table,” and I type in a hexadecimal number, because I had a lot of small functions that I’m using as examples. But it only works for small functions, the ones that I want to type in the truth table. Then I’ve got a big function like, “Multiply all pairs of 8-bit numbers.” This is a function of 16 variables—there are 8 bits in x and 8 bits in y . So I write a little change file that takes out this interactive dialog and replaces it with a program that makes a truth table for multiplication.

Then I changed that by saying, “Let’s read the bits from right to left instead of from left to right, which gives you a different BDD.” Or, “Let me try all Boolean functions of six variables and I’ll run through them all and find out which one has the largest BDD.” But all of these are customizations of my original thing.

I’ll have maybe 15 variants of that program that are easily understood. This was an unexpected spin-off from literate programming because of our need for sending out master files to a lot of people that were changing it for their own system; I’m now using it in a completely different way.

Seibel:It seems sort of obvious why that would be useful for you in the kind of work you’re doing, where you want to do a lot of variations on different themes.

Knuth:Yeah, I’m writing a book.

Seibel:Do you think this mechanism could be more broadly applicable?

Knuth:I have no idea. I’m not sure how it would work if I was in a team of 50 people. But I hope that the idea of an individual programmer writing programs in order to learn something is not a dying breed.

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 CWEBbut I still never have to look at the lower-level things because it’ll flash my CWEBsource as I’m stepping through the program.

Seibel:So that’s a facility built into GDB which CWEBtakes 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.