Grassmann’s Vision, by David Hestenes. “Hermann Grassmann is cast as a pivotal figure in the historical development of a universal geometric calculus for mathematics and physics which continues to this day. He formulated most of the basic ideas and, to a remarkable extent, anticipates later developments. His influence is far more potent and pervasive than generally recognized.”
Effective Interactive Proofs for Higher-Order Imperative Programs, by Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. “We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. […] In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden.”
Objects as Modules in Newspeak, by Gilad Bracha et al. “Unlike its predecessors, there is no static state in Newspeak, nor is there a global namespace. Top level classes act as module definitions, which are independent, immutable, self-contained parametric namespaces.”
You said, nobody loves me
and I said, wanna bet?
the night you can’t remember
the night I can’t forget
— The Magnetic Fields, The Night You Can’t Remember
Searching for Evidence of Unallocated IPv4 Address Space Usage in DITL 2008 Data (PDF), by Duane Wessels. Ouch.
Audio Logger and MP3 Streaming Service, how to run a web radio, djb-style. Awesome use of small tools in a Unixy way.
Mario AI Competition, about learning, or otherwise developing, the best controller (agent) for a version of Super Mario Bros.
Question Suggestions, small voyages into the collective psyche of humans who ask google questions.
NeXTStep Icons Still in OSX Leopard, nice.