The month so far from my last diary entry has been the most stressful month of a year with many stressful months: I feel relieved just to have enough space and emotional energy to be typing this diary entry. To give a taste of my month: on or around the 17th me and my wife were challenged by four thugs on the U1 Berlin underground line, one of who kicked me in the eye, sending me to hospital for two days. That was the second most stressful event of this month... I'm much better now, and am satisfied to say the police have a very good chance of catching them: there are three eye-witnesses, and the police (who have been great; the Berlin police have a not entirely undeserved bad reputation in Germany) want me to come in and look at photos.
Web based proof exchange systems:
I am still very enthusiastic about raph's work here, although I am
disappointed he has used python for the implementation. Apart from
that, I think raph's writings show excellent taste and insight. What I
think he has got right:
- Metamath is probably the simplest system good enough to do the job. I don't think Hilbert systems are the best possible systems from a proof theoretic point of view, but the problem with the more sophisticated frameworks is that none of them are yet ``the right thing'';
- Definitions are the hardest thing to get right in a Hilbert system based framework, and I think here is the place where it is easiest to criticise metamath. Raph seems to have a pretty good grasp of the issues here, which are riddled with subtleties, and doesn't seem bound by doing things the way the experts have always done them, which ensures that his work will be interesting whether or not it is successful.
There have been lots of interesting comments appearing on recentlog, but I've not had a chance to write any responses. I'll try to do this in the next few weeks.
graydon:
Great post!
lkcl:
Nice series of articles on windows and its free rivals. Just a
little point: just because POSIX specifies a file system that doesn't
support interesting permissions models doesn't mean that linux and
FreeBSD can't: both of the have VFS layers that allow them to do just
this sort of thing.
Wishing all advogatans a Happy New Year!