After some more weirdness in my thesis proofs I now try to apply Isabelle/HOL, an automated proof checker, to the whole thing. Might take a while to understand, but I like stuff which has to do with computers.
Ulla needs the presentation for MFCS done by the next weekend, including a nice 5-way rotational symmetric image of dining philosophers. How do you give that in cartesian coordinates? Perl programming helps.
Aikido training as usual. After the training, I have to change busses downtown, exactly opposite the Scientology building. As I always wanted to talk to these people anyway, and they offered their infamous personality test for free. What a better occasion than to get some first-hand experience of this, according to common knowledge, dangerous cult. After reading the wikipedia article a few weeks ago, I had expected some kind of general run-down on every negative point I could possibly have. But either the Sydney branch is simply not trained enough or their computer program really allows good results, even if that'd have been a scientific test, I couldn't complain. But I had a nice talk with the evaluator, who rather predictably tried to convince me to buy one of their books — and also rather predictably failed. But according to him, they now try to put their books in public libraries. I'll probably have a look, just to know what's in there, without funding their obscure activities.
Rob has left for the Burning Man festival in USA, hence I'll have to work on my own the following week. Much time to fiddle with the proof checker.