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
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
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
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
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
We were talking about blogging yesterday, and together singing
fragments of the Kipper
theme song, with the words "Kipper the blog".