Older blog entries for raph (starting at number 341)

Sleep

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.

Xr, fonts

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.

Formalism

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.

Languages

I have a confession to make. I've been designing programming languages since I was nine years old (the very first was syntactic sugar for 8085 assembler). Most of them have never been observed in the wild, but one seems to have escaped and taken on a life of its own. Now, I find that there's an implementation of "99 bottles of beer" in it, as well as an interpreter written in OCaml.

I am no longer excited by Io; continuations seemed a lot more interesting when I was a teenager than now, although it is of course useful to know how to program with inverted flow of control. It is, perhaps, a useful illustration that continuations, like a number of other language primitives, are powerful enough that you can build an entire programming language from them and nothing else.

Also, I enjoyed chromatic's essay What I Hate About Your Programming Language. I tried responding on the comment page, but it wouldn't take my login. I'm sure the login problem is due to the website being written in some dynamic language that encourages messing with stuff, rather than good ol' C, which requires you to think through what you want the code to do first.

Seriously, while chromatic's mention of mod_virgule as a website written in C is gratifying, if I had to do it from scratch, I probably would use Python. I like programming in C (especially deep algorithms), and I like programming in Python (especially prototypes, and gluing things together).

Hacking is like painting

Paul Graham has a fine new essay entitled Hacking and Painting. It's very dense with ideas, and does a good job of describing the flavor of creative programming, something difficult to get across to a mass audience.

Hacking is like painting in some ways, but the analogy breaks down in others. Here's my take on some of the points.

If you want to hack, or paint, get a day job. In hacking, as in painting, it is very difficult to find a situation that rewards artistic accomplishment directly. Business and academia reward something that's different enough to be frustrating. I think that many people had the hope that the explosion of "open source business" would solve this problem, but it hasn't. The "day job" works for painters, musicians, and other artists, and is a good model for hackers as well.

Studying works of art is vital to learn to do art. The great painters learned by studying and copying other great painters, and refining the ideas. One of the best criteria for being a good writer is reading voraciously. Yet, as far as I know, it's rare to teach computer programming by studying great programs. Historically, a big part of the problem was the dearth of great programs available for study. Free software fixes this problem. I considered myself a hotshot programmer before getting involved in free software, but grew enormously through reading other people's code. I'm not sure how much code people study in academia; the Lions book is certainly one early encouraging example.

But: paintings last a long time, code rots fast. In museums and reproductions, we enjoy a body of work going back hundreds of years. In many ways, these old paintings are better than the work of today. Yet, with few exceptions, code that's hasn't been maintained for more than a year or so is dead. One such exception is code that performs a well-defined ask, and does it well (such as libjpeg). Another such exception is "retrocomputing".

Getting the spec right is more important, and more interesting, than implementing the spec. Once you've got a good spec, any competent programmer can implement it. (this is a good working definition of competence :) But coming up with a good spec is very hard. Usually the best way to do it is to incrementally refine an implementation. It's the same for painting - X-ray analysis frequently reveals things painted over and reworked. Oil paints are good for this kind of reworking. Analogously, dynamic languages are better than static languages for this kind of process.

There's a lot of discussion in blog land about static vs dynamic languages, and I expect to return to the topic. I consider programming in C to be like sculpting in marble, and programming in Python to be like sculpting in clay. They're both worth doing, but for different kinds of work. Also, giving a chisel and block of marble to a newbie sculptor produces similar results to a newbie C programmer: a pile of marble chunks covered in marble dust. Paul uses the similar analogy of drawing in ink vs pencil.

Programmers envy mathematicians too much; they should aspire to be more like artists. I see Paul's point here, but in the long run I disagree. Paul uses the analogy of paint chemistry as a scientific theory underlying painting, in much the same way that computer science theory underlies programming. But I think the analogy breaks down. Paint chemistry is obviously useful in predicting the appearance of colors, the way they'll interact with each other, the brush and the canvas, and other important stuff such as glossiness. But the limitations of paint chemistry are equally clear - as a theory it speaks not at all to composition, emotion, or the infinitely subtle issues of aesthetics.

But where are the corresponding limits in the theory of computer programming? This is an open question; certainly many attempts to apply mathematics to real programming have been disappointing. But I think this is because mathematicians aren't good at doing the kind of mathematics needed for programming, the kind where the spec (or the "theorem to be proved") is extremely complex. Indeed, the theorems most highly valued in mathematics are those where the statement of the theorem is very simple, but the proof is deep (Fermat's Last Theorem is a shining example).

Fortunately, there are people exploring that edge, "proof hackers" if you will. Metamath, HOL, and proof-carrying code represent some of the most interesting work in that direction. If these people succeed in expanding the useful scope of mathematical technique, then it will dramatically change the way we do programming

In this distant future, the use of mathematics will depend greatly on the type of programming being done. Aesthetics will still be important (without question in any area that deals with human interaction), but for well defined tasks and well defined properties (especially security properties), the best programs will be provably correct.

tree ISA vehicle

I see yet another suggestion that Max has the hacker mind. The other day, he discovered an undocumented feature in "Reckless Drivin'" - if you press the Alt key while clicking on Start, it pops up a dialog box that lets you choose a vehicle number.

So we started going through the numbers, and he enjoyed being able to drive cars, buses, go-karts, helicopters, and so on. Then, we found a vehicle code that corresponded to a tree. In a 2D driving game, it makes sense to consider a tree as a type of vehicle; it's rendered the same way, and even though it doesn't share all methods, it's probably easier to just leave methods for motion unimplemented than to branch out the class hierarchy.

Anyway, when Max saw the tree, he thought it was very funny, and laughed out loud. Was this because he saw a glimmer of the design of the program, and found the incongruity between the internal "tree ISA vehicle" and the real world, or is he just a happy kid who likes to laugh? Either way makes me feel good.

Urgh, haven't updated in a while. Last weekend, we went to a Quaker retreat at the beautiful Ben Lomond Quaker Center, and then the next few days an Artifex staff meeting.

RH 9, fonts

My laptop's hard drive failed (another quality product from IBM :). This time around, I decided to install RH 9 from scratch on the new drive (it was Debian before).

So far, I like it. I miss apt-get, but more stuff seems to just work. Also, the antialiased fonts are a nice big jump. I am sad that support for subpixel positioning isn't there yet, though. In general, you can get away with integer quantization on the widths when you're doing imprecise text layout (GUI labels and HTML rendering, as opposed to, say, PDF), but there are still definitely cases where the spacing gets wonky.

As far as I know, there is only one text rendering engine that does antialiasing, hinting (specifically, contrast enhancement by subtly altering the position of stems), and subpixel positioning: Acrobat (Reader) 5. Mac OS X does AA and subpixel, while RH 9 (by means of FreeType 2) does AA and hinting. I'm looking forward to the first free software implementation of all three.

At the staff meeting, we've decided not to move forward with our funded project to integrate FreeType as the font renderer for Ghostscript, rather concentrating on improving the existing font renderer. I'd still like to see the FT integration happen, though. The best outcome, I think, would be to recruit a volunteer from the free software community to take over this project.

Fansubs

I've discovered anime fansubs. These are basically Japanese anime shows, with English language subtitles added, then encoded (usually to MPEG-4) and distributed over the Internet. Their legal status is murky at best, but a sane code of ethics prevails: fansubbers release shows that have not been licensed to English-speaking markets. Under this code, everybody wins. Copyright owners of shows don't lose revenue directly, because there isn't any from those shows. Indeed, it's likely that popularity of the fansubs fuels interest in official licensing. And, of course, viewers win because of access to great shows like Hikaru no Go, which would otherwise not be available, or only at great difficulty. Alan has started watching Naruto (I still read the subtitles aloud to him, but I'm sure his reading speed will catch up soon), and enjoys the insight into Japanese culture as well as the Ninja-themed action-adventure storyline.

The best of the fansubbers do really good work on the translation, subtitling, and other stuff; arguably much better than many "official" versions. I think Hollywood could learn much from their example.

People leaving

I've been feeling a bit down the past few days. The departure of some good people from Advogato is probably a factor.

I want this to be a good site, and bring people together as part of a community. I know I can't please everybody all the time. But I am wondering if there are some basic things I can do to make this a more congenial place.

First, I deliberately chose a light touch for applying the trust metrics. They're basically opt-in, especially the more recent diary ratings. I had thought that users of this site would have a fairly thick skin, and that simply giving people the tools to filter out stuff they didn't want to see would be sufficient. But perhaps that assumption isn't right. Maybe the default should be to present the recentlog with a trust metric computed relative to a "seed", so that most people wouldn't see low-ranked entries unless they deliberately chose to seek them out.

I've been thinking of doing something like that for an RSS feed of the recentlog anyway, as there aren't good client-side tools for filtering those. So the question is: would stronger filtering bring back the people who left? Is this an important goal, in any case?

There's always been a tension between people wanting to find their own blog hosting, or have them hosted here. As a blog host, this site has been fairly minimalist, although I can definitely see adding in the really important features over time. But perhaps it's more distributed, more Web-like, for each person to be responsible for their own blog hosting, and use other tools to integrate blogs from disparate servers. In the meantime, I think our recentlog provides a useful and interesting mix of individual postings and communal discussions.

Inline functions

After some more thinking, I don't really like the DEF_INLINE macro I wrote about last time. The simplest approach, I think, is to define the "inline" keyword to that of the compiler, or, if the compiler simply doesn't support inlining, then to the empty string, so that each .c file that includes the .h with the inline functions gets its own static copy. An interesting question is: are there any compilers in widespread use today which do not support inlining? Certainly none of the ones I use.

Inline functions in C

I was looking again at the question of how to do inline functions in C. There's a relatively recent page by one Richard Kettlewell, but it doesn't quite explain how to do inline functions really portably, in particular so that code will work correctly on compilers which don't support inline functions.

I think this goal is achievable without too much pain. Here's a sketch.

1. Guess conservatively whether the compiler has a keyword for inline, and define it to be "inline". Here's a sketch:

#if defined(__GNUC__)
#define inline __inline__
#elif defined(_MSC_VER)
#define inline __inline
#elif !defined(__STDC_VERSION__) || __STDC_VERSION__ < 199901L)
#define DISABLE_INLINING
#define inline
#endif

An enhancement of this code would be to detect the cases where autoconf is able to detect the compiler's support for inline and report it in a "config.h" file or the like. See, though this mail for a cautionary note.

2. Set up a DEF_INLINE macro. This macro makes an inline definition when available, otherwise a standard function declaration:

#ifdef DISABLE_INLINING
#define DEF_INLINE_BODY(proto, body) proto { body }
#define DEF_INLINE(proto, body) proto;
#else
#define DEF_INLINE_BODY(proto, body) static inline proto { body }
#define DEF_INLINE DEF_INLINE_BODY
#endif

3. Then, in your .h files, define your inline functions as follows:

DEF_INLINE( void unref(obj *o),
    if (--o->refcnt == 0) destroy(o);
)

4. Now for the slightly tricky part. In one .c file, include the following fragment:

#undef DEF_INLINE
#define DEF_INLINE DEF_INLINE_BODY
#include "yourfile.h"

A possible enhancement is to set DEF_INLINE back to its old value, but if yourfile.h is the last included file, it's just more code.

This approach has the advantage that you can disable inlining with a simple switch. This might be handy for debugging (for example, setting breakpoints in the inlined function), and also to measure the performance improvement actually achieved.

The drawback, of course, is the use of the C preprocessor. It's too easy to try to create your own language using C macros, and often a bad idea.

If you only care about GCC, MSVC, and C99 compliant compilers, you can get by with just step 1. In fact, it'll probably still work on older compilers, but with the downside of replicating the "inlined" functions in every .c file that includes them.

It's a shame that such a simple and valuable feature is such a mess when it comes to standards and actual implementations. Ah well.

RSS export

Advogato diaries now have RSS feeds. Here's mine. I've checked it with some validation services, but don't really know how well it works.

The DRM struggle

The recent Xbox hack provides further evidence for a widely held belief in hacker circles: real DRM is technologically impossible, at least without huge improvements in the ability to produce bug-free software. Zooko writes passionately that the bad guys may well be winning anyway.

Indeed, the important distinction here is whether freely accessing digital content is convenient or merely possible. If a DRM scheme makes access inconvenient for most people, then it has largely succeeded in its economic goals.

Technologists, and free software hackers in particular, should be careful not to underestimate the importance of convenience. Over the next few years, I think that one of the most compelling applications for free software is a media player that just works, especially without stumbling over harebrained DRM schemes. The underlying technology is mostly here now, including the ability to efficiently move bulk files around over consumer Internet connections. But unless it's easy enough for your mom to use, it won't have much impact.

Essence of XML

I got my POPL proceedings a few days ago, and found Jerome Simeon and Phil Wadler's The Essence of XML to be one of the most interesting papers. He writes:

So, the essence of XML is this: the problem it solves is not hard, and it does not solve the problem well.

In particular, the paper is about type systems for XML, which include DTD's (widely recognized as underpowered), XML Schema, and other proposals. The paper goes into XML Schema in some detail. A central observation is that, while XML Schema obviously intended to provide for unambiguous schemas, it failed to acheive this goal.

The W3C produces mediocre standards. Not so bad as to be unworkable, but certainly not crisp and beautiful either. In many ways, this is better than anarchy, because at least they are standards, and there is a ton of code out there to deal with them. Lisp S-expressions may be prettier, but there are still plenty of details you have to nail down for compatibility, including choice of charset, dealing with string quoting, and so on.

mod_virgule

By popular demand, I've started hacking up RSS export for diaries. It's a little harder than I thought it would be. There are two bits to get past to make it validate, then perhaps some impedance mismatch. One of the bits is conversion from ISO-8601 dates (which is what mod_virgule uses internally) to RFC 822. Another is conversion of relative URL's within diary entries to absolute. Both of these are SMOP's.

The impedance mismatch is that Advogato diary entries don't have a designated title field, and the "description" can be very long. Many people (myself included) follow the convention of titles in <b> tags, but it seems dangerous to rely on this for structural information.

Probably the thing to do is just export the full entry as the RSS <description> for now, and gradually move to the option of more structural markup. I've been wanting to do something similar to provide summaries of mid-rated diaries in the recentlog anyway.

Thanks to dyork's reminder, I've updated the Wiki intermap. Also, I see that Gary did some code towards displaying multiple entries from a single poster in the recentlog. Hopefully, we'll be able to get at least the minimal amount of maintenance done soon.

Life

The last couple of weeks have been really hard on my productivity. I feel like I've been getting behind on a bunch of things, including design and coding work on Fitz, the IJS 1.0 spec, a command-line version of the trust metric, and other things.

I'm feeling a bit more productive now and hope to catch up over the next few weeks.

Proofs

During times of stress, I find it comforting to muse on proofs. The idea of mathematical certainty, is soothing to me.

Much of my thinking is directed towards a scheme for portable and modular proofs. For one, there are many different axiom systems, of various strengths. Most proof systems simply choose one. The problem with this is that proofs can be ported to a system with a stronger axiom system, but not in general to a weaker one.

Further, if you have a minimalist set of axioms (such as second order arithmetic or Zermelo-Fraenkel set theory), then you want to construct a rich library of objects (many flavors of numbers, sequences, functions, etc.) on top of it. In many cases, there will be more than one viable construction (for example, reals can be infinite binary expansions, Dedekind cuts, or the Harrison's clever HOL construction). Proofs shouldn't depend on the details of the construction used. A proof over the reals should go through exactly the same no matter which construction of the reals undergirds it.

So I've been thinking along the ideas of modules and interfaces. The axioms of complex arithmetic would be one example of an interface. A proof over complex numbers imports this interface. A module representing a construction of complex numbers would import the HOL primitive axiom interface and export the complex number interface.

Each module can be checked individually, to make sure that the exports are justified in terms of the imports. Then, you can check a whole pile of modules, by instantiating the abstract interfaces in each "import" and "export" with concrete replacements. For example, the abstract addition function is replaced with a definition appropriate to the chosen construction. The whole thing checks if each import (after instantiation) is satisfied by a matching export (again, after instantiation) from a previous module (ie, no import cycles allowed).

Thus, you could fairly easily check a proof over complex numbers in any one of the axiom schemes powerful enough to represent them. Just supply the construction appropriate to the primitive axioms.

Not all proofs will check in all axiom systems, of course. In general, a proof module should be conservative in what it imports, so that it will check in the largest range of axiom systems. This principle also ensures that proofs can be ported to the widest range of other systems.

I hope to write about these ideas in more detail, including why it's important. It's obvious to me, but other people seem to need convincing. That sounds quite a bit like Ivan Sutherland's recipe for successful research: do something you think is easy, but everybody else thinks is hard.

28 Mar 2003 (updated 28 Mar 2003 at 06:37 UTC) »
Other blog : Notes on the "Saddam prepares to flee to Syria" hoax

332 older entries...

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!