This week I learned...

Special double issue! Two weeks' worth of trivia, including a week spent in Mountain View.

• Most Japanese streets do not have names.

• With GNU Radio, you can buy some cheap hardware, plug it in, and your computer becomes a GPS receiver, a garage door opener, an HDTV tuner, an AM/FM radio, a cell phone. This is subversive technology. Hollywood wants regulations that would ban such nonsense.

• Radio waves bounce off meteor trails. This is actually usable as an alternative to satellite communications, depending on the application. For example, the USDA has a network of solar-powered snow depth sensors that use meteor trails to phone home.

• On the Mac, Alt+[ types a left double-quote mark and Alt+{ types the right one. Much better than typing “.

• GCC generates a floating-point instruction for isnan(x); it amounts to x != x (NaNs are not equal to themselves). Intel engineers claim integer instructions can be much faster, on x86 at least, due to floating-point exception nastiness.

• Xavier Leroy has written a provably correct “lightly-optimizing” back-end that compiles a subset of C to PowerPC machine code. Sandrine Blazy and Zaynah Dargaye have hooked it up to a provably correct front-end.

  A little background here. A compiler works by lowering code step by step from relatively high-level internal representations, like parse trees, to successively lower-level representations, until it gets down to machine code. At each level it can apply optimizations: some optimizations, like common subexpression elimination, work at a very high level, and some work at the machine-code level. Stack up enough lowering passes and optimizations, and you've got yourself a compiler. There's considerable interest these days in using formal methods to prove the correctness of program transformations. First you define mathematically what it means for two programs to be equivalent. Then you prove that a given transformation always produces a result that's equivalent to the original. Stack up enough provable lowering passes and optimizations, and you've got yourself a provably correct compiler.

  This kind of work has been done for subsets of Java, but C's pointers and undefined behavior present some nasty problems. Leroy's work is hedged in with disclaimers, but it's still pretty amazing stuff, and an interesting read. For example, he proposes the following sneaky technique. Write your compiler pass however you want, and don't bother proving it correct. Then just verify the correctness of the transformation afterwards (for the particular program being transformed). It's apparently much easier to prove a verifier correct than the transformation code itself. Plus, you can then tweak the transformation without redoing any proof work. The only risk is that your transformation is incorrect, in which case your compiler flunks out with an internal error at compile time.

• The PDP-11 had probably the nicest of all the widely used CISC instruction sets.

• emacsclient is my new EDITOR. It connects to my existing Emacs process, if any (I had to put (server-start) in my .emacs file) and loads the file there.

• Speaking of emacs: M-/ is the autocomplete key. It's moderately smart. You also want to know C-x r SPACE x (save current cursor position in x) and C-x r j x (jump to the position saved in x).

• When you run a configure script, it generates a config.status file in the build directory. That file is helpful when debugging stupid build problems.

• In the late-1990s, there were two computer science research projects called Dynamo, both involving dynamic optimization: one at Indiana University and of course the awesome one, at HP Laboratories.