In it, he points out the logic advocated by Eric Hehner. In this logic, programs themselves are predicate expressions. Graydon claims that this results in some simplification, presumably because you don't have to separate two different kinds of expressions: programs and predicates about them. Hopefully, when Graydon and I meet, he can explain this to me. I suppose it's possible, but to me these do seem like the kinds of things that should be separated.
Aaron Swartz linked my memorial to Dijkstra. It really made my heart glow when he called it "beautiful". Thanks, Aaron.
I got an exciting email a couple of days ago. Somebody smart (you probably know the name) is working on the spam problem, and asked me about trust metrics. I'll post more as soon as it's clear the person wants this info public.