The 7.32 beta release is now official, with Windows and Macintosh builds as well. Hopefully, this means that 8.0 is imminent.
Thanks to everyone who's been helping with this, especially my colleagues at Artifex Software. It feels really good to be part of a team.
If you're in the US, please vote today. Especially if you were inclined not to vote, please consider voting for your Green candidates. The California governor's race is particularly ugly. From the major parties, we have an incumbent who's proved excellent at finding the line between merely aggressive fundraising and outright bribery; and a challenger whose inept campaign hopefully not a predicter of his performance in office should he win, not to mention his closeness to fraudulent practices in his family firm.
By contrast, Pete Camejo is somebody you can vote for without having to hold your nose. A strong showing for him will send an important message that many people are not satisfied with the status quo and want something better. In addition, he has a lot of good experience with finance and ethical issues in particular, which suggests he would make a good governor in the extraordinarily unlikely event he wins.
Davis is sufficiently ahead in the polls that you should feel comfortable voting for Camejo even if the thought of a Republican in the governor's office disturbs you. Even so, I'm more inclined to vote for the best candidate than the lesser of two evils in this election.
Please consider your Green candidates in local races as well. Green candidates can and do win offices at the local level, and these are often positions where they can do some good.
But no matter what your political beliefs, vote. It's how our democracy, however flawed, works.
Proofs and Types
chalst: Hrm. Unfortunately, Girard's book is just a little over my current threshold for accessibility. At this point, I really prefer Web-available resources, as well, largely because I am doing this as a weblog and want to encourage other people to follow along.
I know I've just labeled myself a lazy student, but I'm wondering if you could give me some hints nonetheless. You mention Z_2-style and Coq-style consequence relations. What is the big difference between them? I'm not used to thinking about logical systems in terms of the consequence relation, but do know what the term means. Of course, I know one difference is that Coq is intuitionistic, but I think that's not the main thing you're talking about.
I'm also having a little trouble grasping the idea of a lambda calculus with the same strength as Z_2. Is the trick to write functions as finite strings, analogous to a computer program to compute the function? This way, you quantify over computable functions rather than the imaginable universe.
PS: chalst: Michael Norrish has some notes he'd like to send you, but doesn't have a working email address.
I don't feel like I have much extra time to write, but I've been thinking of doing a longer essay on some of the controversies in mathematics, especially as they're relevant to proof systems. The most important ones are logical strength (from primitive recursion to ZFC, with at least Z_2 and HOL as way-points, and specialized need for systems past both ends), types vs. no types, and partial functions vs. total functions. In the "moderately important" class I'd put classical vs. intuitionistic logic. The philosophical issues don't do much for me, and it seems like it's almost always possible to work around the intuitionism when you need to. Finally, in the least important category, I'd put choice of primitive operators and axioms for the propositional calculus. They're all quite equivalent, but that doesn't stop people from arguing their favorite.
Hmm, I wonder whether this is a reasonably complete list, or if there's another big one I'm overlooking.
Trust metrics for spam-free blog comments
Dave Winer talks about a large-scale single sign-on system for posting comments and replies in blogs. In this entry, he mostly talks about the convenience factor of not having to type in passwords and other information all the time.
At the same time, there's a lot more awareness of the vulnerability of comment and reply mechanisms to spam, trolls, and other forms of abuse. So far, the blog world has been quite civilized, but as spammers become tuned into the prestige and popularity of blog placement (not to mention their role in boosting Googlejuice), this will undoubtedly begin to change. Heather likens it to the Internet pre- and post-AOL.
I just realized today that both problems can be solved quite easily using the trust metric technology that powers the diary rating systems in Advogato. Blog servers, acting as clients to this new service, would get a cookie from the user's browser (probably using Passport-style techniques), and get an auth token back, also with a one-to-ten ranking, if so desired. This way, anyone who's hooked into the blog world can post comments and replies, but abuse would be limited.
In a dream world, we would have a decentralized peer-to-peer identity service based on a cryptographically sound protocol, but in the meantime there are a lot of people implementing blogs with very crude authentication. I think it will be possible to hack something together quickly.
Once the infrastructure is in place, I can see it being useful for a bunch of other things, including authenticating backlinks, which are also spam-vulnerable. And, once the social net of bloggers starts becoming reified into a net-accessible graph, the stage is set for evolution to a more decentralized system. It seems like a good way to get rapid adoption of the trust metric ideas.
I discussed the idea with Bram and others on #p2p-hackers, and he had some good ideas about how to make a simple challenge-response protocol that would be both easy to implement over the existing infrastructure and reasonably secure against the most common attacks such as password sniffing. He'll probably want to post about that himself.
A couple of days ago, Alan was trying to gross us out at the dinner table, which is of course a normal six-year-old thing. But, being Alan, he tried to convince us that he had "bee larvae" on his plate.
Max really loves his "puter games" and is quite good at running the computer. In particular, he can usually quit out of a game by himself, which is even more impressive considering the atrocious consistency of keybindings in the downloadable Mac OS X games. He seems especially good at reading icons and other visual elements. For example, just today, he got some stickers trying to convey "no sweat" by the international "no" circle overlaid on some water drops. He didn't get it exactly, but we were pretty impressed by his interpretation as "stop raining".
We were talking about blogging yesterday, and together singing fragments of the Kipper theme song, with the words "Kipper the blog".