I just had my second sleep study this morning, and this time they did find some apnea. Next, we'll see what to do about it.
There are a few factors which have changed since the last time, one of which is that I'm 160 lbs now, about 20 more than when I had the first study done. I'm going to experiment with losing weight again, and this time hopefully I'll be able to track any improvements. So, again, I'm interested in putting together a home sleep study. The sound is fairly easy, but it's doesn't give a clear indication of breath cessation. I think the least invasive technique for measuring that is a flow meter, but real sleep studies also add an EEG and a pulse oximeter.
Again, if anyone knows a good, inexpensive source for this equipment, or has experience doing something similar, suggestions are greatly appreciated.
I talked in depth with Keith Packard a few days ago. We spent a fair amount of time talking about font rendering, and also about the Xr project. Xr is interesting - it overlaps in goals somewhat with Fitz, but with a primary focus on interactive display applications.
Among other things Xr gets right is that it's cross platform - earlier Xrender work seemed much more Unix-specific.
I think the question of how to do high quality text rendering on the desktop is still open. One local maximum is the current performance of Xft with the Vera fonts and with TrueType hinting enabled (screenshot). This configuration succeeds in rendering high-contrast, fairly visually uniform text (stroke weight and spacing are quite uniform, but curves and diagonals are softer than vertical and horizontal lines). I personally find the 1-pixel stems to be a bit light, especially on my 132 dpi LCD screen, and in general prefer text that looks a little more like original, unhinted fonts. In particular, I like different sizes of the same font to be roughly consistent in darkness. With Vera, medium-big print is much, much lighter than small (as soon as the stroke weight goes to 2px, then it's darker again).
This kind of rendering is perfectly reasonable for GUI elements and HTML rendering, but not for WYSIWYG viewing (such as PostScript and PDF). For this, I think the tradeoffs shift a bit. Even aside from matters of personal preference, to ensure even spacing you need subpixel positioning. That, in turn, basically forces lower stroke contrast (although not necessarily as soft as completely unhinted rendering, such as OS X). The Xft API doesn't support subpixel positioning, but no doubt a more sophisticated text API for XRender will.
In any case, with all this playing with fonts and font renderers, I've rekindled my own font, LeBe, a revival of a font from 1592. Some of the glyphs still need work, but overall I'm pleased with the way it's going.
Formal proofs don't mean that mathematics is reduced to no more than the manipulation of strings. A proof reflects the personal style of the person devising it, whether or not the individual proof steps can be formally checked. The need to recount the proof steps in detail is a constraint, just as the moves of chess or Go are a constraint.
Mathematics seems to get along pretty well without strict adherence to formalism, but I think that using mathematical techniques for computer programming is a different story. The mathematical content of most relevant theorems is mind-numbingly tedious, so I think you need a computer to check them, and probably to help generate them, for realistic programs.