Book Report: Essays in Computing Science (Hoare)
It's a collection of essays on Computer Science by Tony Hoare, dating from the 1960s through the 1980s. This isn't what you'd expect to find on my reading list, but the essay on Communicating Sequential Processes comes up when you study up on concurrency, e.g., in that Rob Pike lecture lecture on concurrency in Newsqueak. And that essay did explain some strange vocabulary in Erlang, vocabulary like "guards". Where did this jargon come from? From Hoare, probably. Wow, there he is talking about it in this essay right there. It's enough to make the hair on the back of your neck stand on end.
It's good to read essays by the giants of computing. Things change quickly in this field. This means that you can ignore the historical points that you disagree with, while holding up those you do agree with as "timeless truths of eternal verity." I agree with this one, so I'm going to use it to win arguments:
...we admitted that it was the duty of programmers to educate their managers and other departments of the company by "...presenting the necessary information in a simple palatable form." The hope "...that deficiencies in original program specifications could be made up by the skill of a technical writing department... was misguided; the design of a program and the design of its specification must be undertaken in parallel by the same person, and they must interact with each other. A lack of clarity in the specification is one of the surest signs of a deficiency in the program it describes, and the two faults must be removed simultaneously before the project is embarked upon." I wish I had followed this advice in 1963; I wish we would all follow it today.
"The Emperor's Old Clothes"
I skipped most of the book, though. Most of the essays in this book are about proving program correctness. Oh man.
Look, I appreciate that the people who try to prove program correctness are very clever. It's just... it's just... if I'm supposed to learn your notation, and then follow your five-page line of reasoning... if I'm supposed to convince myself that each of these steps is correct, that you haven't made any mistakes (and I'm not sure that I'm clever enough to spot these mistakes; but I do know that cleverer people than you have made mistakes in these proofs...) It's just... it's just that...
Rather than spending the time on a proof, I'd probably be more reassured that your algorithm is correct if you give me a hand-wavy explanation, a demo, and pointed at a few unit tests. I'm just sayin' is all.