Sat 2006-10-14 I've just spent a happy 15 minutes reading the reviews of the RAND Corporation's "A Million Random Digits with 100,000 Normal Deviates" on Amazon (link via Bruce Schneier).
Reading things like this made me realize that the Web is becoming a repository not so much for the wisdom of humanity as for its idle chatter and banter.
Wed 2006-10-11 Steve Yegge has this to say about the programming language Ruby:
I have a lot of trouble writing about Ruby, because I find there's nothing to say. It's why I almost never post to the O'Reilly Ruby blog. Ruby seems so self-explanatory to me. It makes it almost boring; you try to focus on Ruby and you wind up talking about some problem domain instead of the language. I think that's the goal of all programming languages, but so far Ruby's one of the few to succeed at it so well.
I am not experienced enough with Ruby to confirm that this is true for that language but I do recognise the same feeling of falling through the language into the problem domain when using Leslie Lamport's TLA+. I get this feeling much more with TLA+ than with Alloy, but then I am a lot less experienced with the latter.
Mon 2006-10-09 One of the key events in the early development of formal methods was T. J. Dekker's invention of his mutual exclusion algorithm, not so much because of the practical value of the algorithm, which is rather limited, but because of the way Dekker developed it. Edsger Dijkstra tells the story in EWD 1303:
For economic reasons one wants to avoid in a multiprogramming system the so-called "busy form of waiting", in which the central processor is unproductively engaged in the waiting cycle of a temporarily stopped program, for it is better to grant the processor to a program that may actually proceed. This economic consideration was in 1961/62 a strong incentive for the introduction of the P/V-synchronization mechanism, which made it explicit to the scheduler when a program was no candidate for processor time. An in retrospect more profound incentive, however, came from an experience I had in 1959 at the Computation Department of the Mathematical Center in Amsterdam.
I had invented what, in that environment at least, was a new type of problem. Consider two cyclic processes, each consisting of an alternation of "a critical section" and "a noncritical section". Was it possible to synchronize these two processes such that at any moment at most 1 of these processes would be engaged in its critical section? The way in which the processes could communicate was by atomic reads and writes in a common store. After having convinced myself that --at least according to the State of the Art of those days-- the answer was not obvious, I broadcast the problem to the members of the Computation Department for their general amusement and distraction. It was given that each execution of a critical section would only take a finite amount of time and it was required that a process ready to execute would in due time get the opportunity to do so.
Many purported solutions were handed in, but on closer inspection they were all defective, and my friends realized that the problem was harder than they had suspected and that their simple "solutions" wouldn't do. Fortunately my friends didn't give up and they handed in "improved" versions of their earlier efforts. But as their designs became more and more complicated, it became harder and harder to construct a counterexample. I couldn't keep up with them and had to change the rules of this programming contest: besides a program I required a proof that the program had all the desired properties.
And then something profound and lovely happened. By analyzing by what structure of argument the proof obligations could be met, the numerical mathematician Th.J. Dekker designed within a few hours the above solution together with its correctness argument, and this settled the contest.
Proof-driven development back in 1959! Much of Dijkstra's subsequent work can be seen as working out the consequences of the insight that programs should be developed with proof in mind.
Wed 2006-09-27 
For the past few weeks there has been a continual fall of horse chestnuts from the trees around our flats. Every few minutes night and day we hear the sound of one crashing through the leaves and then hitting the ground with a thud. If the wind is up they sometimes hit our flat roof and bounce several times. Occasionally there is a metallic clunk as one hits a car in the grounds of the flats that were built on the neighbouring field; I find this particularly satisfying.
During daylight a flock of between 4 and 10 wood pigeons browses on the lawn out the front and I have several times seen falling conkers landing close to them. The pigeons just look round and carry on pecking at the ground. It wouldn't surprise me to find a concussed pigeon down there some day.
Some of the chestnuts are cleared away by squirrels but by far the most are taken away by humans who seem to be fascinated by them, children especially, but not exclusively: I have seen otherwise quite respectable adults stop and gather them up.
