We had a good family Thanksgiving at Heather's father's house, with her youngest sister also. We had a roast turkey and all the traditional trimmings. Sometimes I'm pretty cynical, but this year all the tradition, and being close to family, felt good.

Yet another letter-quality display

Sharp has introduced its latest Zaurus in the US. It's the successor of the C7x0 series, which had a nice 216 dpi screen, but was only available in Japan. This one looks pretty good. It's got impressive wireless connectivity, a good CPU (400MHz xScale), and, unlike the first widely-available letter quality handheld, runs a decent operating system (it uses a Linux kernel).

It's pretty clear to me by now that handhelds are quickly moving to high resolution displays. The maxed-out handheld and ultralight laptop categories are blending into each other, so don't be surprised to see these displays become even more widespread in the next couple of years or so.

Semantic Web

I've long been skeptical of the Semantic Web. It's always had the feel of academic research to me. Standards organizations are best at codifying existing practice, not at doing basic research, and I haven't been all that impressed by the W3C in other domains either, so I've had low expectations.

Of course, I'm not the only one to engage in W3C-bashing. Lately, Clay Shirky wrote an essay which pretty much shreds the idea of the Semantic Web to ribbons. I've been reading some of the ensuing discussion, and much of it is quite interesting.

If you find Shirky's anti-Semantic Web arguments compelling, please read what Tim Bray has to say on the matter. Tim's been involved with the Semantic Web and the W3C for a long time (he's in their Technical Advisory Group now), so you could say he's not an impartial observer. But his essay is a skeptical, hardheaded look at what the first step toward a real semantic web is likely to look like.

I want to make one observation. The metadata Tim talks about (roughly, the kind of data you find in corporate annual reports, only fresher and potentially more detailed) does not have a serious trust issue. In general, corporations will post their own data, and they will be accountable for any errors. Nothing on the Web is really free of authenticity problems, but this kind of data is as close as it gets.

I think this property is important, and stands in stark contrast to most of the metadata you might be interested in. For example, a really nice piece of metadata would be "e-commerce store X has excellent customer service / an alarmingly high rate of complaints." Since this particular bit of metadata is likely to have a significant effect on the flow of revenue, the incentive to manipulate it is simply too great for amoral businesses to resist. People manipulate Google for much the same reasons, and with pretty good success, even though Google has sophisticated mechanisms in place for resisting such attacks.

If the Semantic Web is to become a general tool for automatically generating useful inferences, rather than merely a research toy, the questions of how to make sure the metadata is trustworthy will have to be resolved. I think that's especially true for the more AI-like goals of the project. In the mean time, I think there is much lower-hanging fruit, as Tim Bray describes; data which inherently has a lot of structure, and clear criteria for authenticity and accuracy, but which is now published on the Web in a hodge-podge of flashy web-page formats.

Proof systems

I stumbled across Yet Another Proof System. This one looks still somewhat embryonic, but still possibly interesting. I'm definitely not convinced that the GFDL is the right license for mathematical proofs. It's gone through a few name changes recently, but it was interesting to see the similarity between one of their recent ones, "Hilbert II", and Ghilbert, the name of my toy proof system.

Meanwhile, my system is steadily gaining capabilities. It now accepts the entire set.mm of Metamath (translated into Lisp-like syntax). I've also got a Python program which can prove statements of the form "x + y = z", where x and y are arbitrary natural numbers (currently expressed in binary). I'm also playing with axiomatizations of Z2 and HOL, and indeed have been able to prove the first dozen or so derived inference rules in Chapter 8 of the HOL System description (Kananaskis version). If I can get two major axiom systems to connect in some meaningful way (so that proofs in one can make use of theorems in the other), that would be cooool.

Video jukebox

I want to get one of those little low-noise 1GHz Via C3 systems for the family this Christmas. I'm not so concerned right now about the software it'll run it (in particular, it's not essential to record video off-air, nor provide splashy on-screen graphics). On the other hand, it must run MPlayer, output to NTSC video, and have 802.11b. I'd really like it to run Linux, but I understand that certain things like video-out can still be a bit painful. An outboard VGA->NTSC converter would be the easiest way to solve that problem, but I worry that it might not deliver quite the quality of a direct NTSC output, especially when it comes to smoothness of motion.

Has anyone here successfully put together such a system? I'd especially like recommendations for things that work smoothly with a Linux kernel, and/or recipes for configuring the pieces to work together. I'll happily post the winning recipes when I get the stuff going.