**Bad Code**

Reading Dijkstra's obituary, I realized that I've always viscerally thought of structured programming as a concept which has always existed, and always been obvious. In fact it was a great triumph of engineering, and one created within my grandparents's lifetime.

My own method of programming is such that I cannot fathom writing code without having a proof of correctness in mind. Prove first, then type. Unfortunately programmers seem to fall clearly into one of two categories - those who can't program without thinking about proofs of correctness, and those who can't think about correctness proofs at all. Sadly, the second type seems to be dominant, with disastrous consequences for code quality.

Interestingly, Dijkstra mentioned at the end of note 1308 that the phrase 'considered harmful' was coined by Niklaus Wirth.

**Continue Not Harmful**

Many people incorrectly take the problems with gotos to mean they should avoid other advanced control flow structures, these include -

- break
- continue
- return (from the middle of a function)
- while true (implicitly using one of the above)
- for/else (a pythonism, else is executed if no break happened)
- finally

All of the above except finally are completely sound control-flow techniques, and you should use them whenever it results in more concise code.

The unifying abstraction to all of them is that each execution point in the program has an expected state of the call stack, so to go there you pop your own state off the stack, then push expected state (an exception or return values) back onto the stack, and then jump.

Exceptions are interesting because they decide how far back to pop the stack dynamically. The way most languages conflate exception identification with the class hierarchy is kind of a hack, but works acceptably.

'Finally', on the other hand, is a conceptual mess. I pity anyone stuck debugging memory leaks in a non-garbage-collected language which are triggered by a finally clause raising an exception of its own.

**Golomb Rulers**

The exhaustive search algorithm which ogr uses can probably be improved a lot. In essence, it recursively starts with a ruler with some positions marked and some positions consequently ruled out, and branches on whether or not a given position is marked.

The technique it uses for picking which position to branch on is to pick the smallest available one, which is awful. In general, we wish to branch on a spot which is likely to be proven to not lead to a solution as quickly as possible. Always using the least available position causes positions towards the beginning to be ruled out redundantly and positions towards the end not to be ruled out until very late. In particular, none of the positions in the last third will be ruled out until a position is marked outside of the first third.

Better techniques include picking the position which rules out the most available spots, and picking one (pseudo)randomly. These techniques carry significant overhead, so it probably makes sense to branch on the last few marks by picking least available, but they are clearly warranted for the first few marks.

Unfortunately, the last few exhaustive searches for optimal golomb rulers have just verified the previously known best solutions. Ah well.

**Ceci n'est pas une Pipe**

fxn: I am using the word *interpretation* for what it means in english, a meaning it has had since long before it was ever used in mathematics. The value 1 + 1 + 1 in PA, viewed completely abstractly, has no more to do with our concept of 'three' than it does with the planet mars. Only with interpretation does the statement 1 + 1 + 1 = three have meaning.

I'm of the opinion that the natural numbers are the main impetus for trying to make mathematics formal in the first place. Every time a new basis for mathematics is devised, the very first thing which is done with it is to build the natural numbers. Mathematics is a slave to our concept of the naturals, not the other way around. On the other hand, there is no generally agreed upon interpretation of the statement *the real numbers are compact*, and that disturbing problem lies in the dark corners of even such mundane subjects as high school geometry.

I have a confession to make. I don't *really* believe in anything other than PA. My interest in foundations of mathematics is mostly a morbid fascination with the possibility that important new results will strongly depend on large cardinal axioms or worse. I don't really even believe in Goodstein's theorem. Sure, I'll happily talk about it as if it's true while sitting in the safety of my own home, but if I had the opportunity to take a joyride in a spaceship whose engineering soundness I had full confidence in except that it depended on Goodstein's theorem to not go spinning out of control, my feet would remain firmly planted on the ground, thankyouverymuch.

I do, however, believe in the planet Mars. I would even go so far as to say that it exists.

**I said a boom-chika-boom**

Chicago: The order in which explosions are done does not, in fact, matter. Proving the following is an interesting exercise -

- A never-ending explosion must take control of the entire board.
- It is impossible for the entire board to be filled with pieces of one side and it be the other side's turn (this would result in there being no legal move).

I could add logins and rating and other games and such to my Boom Boom implementation reasonably easily, but have decided not to. That could easily become a time pit, and there are already underutilized games servers on the net. For example, there's the excellent Newton Games, which includes my favorite game, hex.

With regards to angel vs. devil, I haven't come up with any strategies for the devil which go much beyond the ones given in winning ways, which show that, for example, the devil can force the angel to make a single turn which involves moving downwards.

**UI snit**

Whenever I'm editing an already posted diary entry I always blanche at hitting the 'Post' button because I'm afraid it will double-post. It would be better for it to say 'Update' in that case.