4 Oct 2002 raph   » (Master)


The quest for a good VoIP solution continues. One step which may be considered either encouraging or discouraging is TeamSpeak. Most importantly, it's not free software, but it does seem to work well enough to use. It comes from the gamer community rather than any existing VoIP constituency, which leads to some funky terminology. When someone joins a channel, a sci-fi female voice announces, "new player." On the plus side, there's an emphasis on performance and usability (especially with NAT's, which basically Just Work).

I do want to try GnomeMeeting again, but so far it hasn't worked for me. One of the most encouraging things about GM is that the next version will support the new Speex codec, which basically does for voice what Vorbis does for recorded audio. I took the standalone coder for a spin and was very pleased.

Proof-carrying code and code-carrying proofs

Michael Norrish sent me a nice email on my recent entry on proofs and code. The question of whether the proof checker should include a virtual machine, so that proofs can include programs is in some ways the dual of proof carrying code (and bib from 2000), in which programs come in "fat binaries" with proofs attached. A runtime can then check the proof, and execute the code with some assurances, primarily safety. PCC obviously needs a good, clean, efficient proof format, and equally obviously motivates a sharp separation between proof generation and proof checking. It's worth following.

Code-carrying proofs are by no means a new idea. In fact, Coq already implements them. It's not clear to me how deeply they're actually used. Among other things, you'd think they'd be useful for avoiding size blowup when importing theorems from other systems, but at least Freek didn't seem to use this in his HOL to Coq translator (Encoding the HOL Light Logic in Coq).

Translations between proof frameworks

When you look for it, there's been quite a bit of work done on translating from one proof framework to another. HOL has been translated into both Coq (and see another prototype) and NuPrl. These are not unique, although as it happens such translations can be quite tricky. For one, logical systems really do differ in expressive power. This is a bit unintuitive for those of us who grew up on the Church-Turing thesis, which effectively states that all programming languages have the same expressive power, because you can always write a translator from one to another. But logical systems differ in, for example, the number of ordinals. A proof that so-and-so-many ordinals exist can be ported to a "larger" system, but not to a "smaller" one. I can easily imagine a network of such formal systems, but I do not know how to draw the arrows. For example, I'm pretty sure that you can represent HOL in ZFC set theory, but my hunch is that the reverse is not possible.

However, I think a lower-tech solution may well be practical. Not all proofs make use of the full power of the logical framework. If a specific proof only uses the subset common to both frameworks, it should probably be portable.

I think this issue is related to the way Metamath nails down constructions. Since other systems naturally choose different constructions, you clearly can't just port proofs over. In Metamath, you can add sets and integers and get meaningful results. Obviously, porting any such proof to a different system will fail. However, if a specific proof uses only the integer axioms, and doesn't refer to the construction directly, it should be portable.

The way forward seems to be a significant portable library of the basic constructions: integers, reals, pairs, sequences, trees, etc. These basic constructions should be done in the most natural way in the framework. Then, when importing proofs, you hook up these constructions. There are some subtle details, mostly around partiality. What exactly is 1/0?

Proof efficiency

Another concern Michael raised is the relative inefficiency of a translated proof. Especially in the HOL framework, small proofs in the "source language" (which is really ML with a nice library) expand out to a large number of primitive inference steps. In the usual HOL scenario, the inference steps go very fast. If you're writing them out to a file, then sending it over the net to a different system, you might start caring about how many steps there are.

I'm not very concerned about this, for a number of reasons. For one, I believe it should be possible to greatly optimize the resulting proofs. For two, storage and bandwidth is relatively cheap and is getting cheaper. For three, a special-case data compressor is likely to be very effective, if one is needed.

But it's not clear one is needed. Both Automath and Metamath have significant libraries of theorems, and both can be checked on modern hardware in about a second. To me, this suggests a huge amount of safety margin between the optimal and the acceptible.

Latest blog entries     Older blog 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!