Self-inforcing protocols

Interesting article by Bruce Schneier:

I especially like the property tax example.

cat flap

I learned this week that Newton invented the cat flap.

LSUIPresentationMode change

I've been using the LSUIPresentationMode trick to hide the Mac toolbar for most applications.  With the latest update, it doesn't look like you can set the number to 4, the options being strings.  You need to now right click and select Show Raw Keys/Values in order to set the number to 4.

Best quote(s) of LFMTP

I think it's a tie

1) Gilles: Higher order matching with dependent types is undecidable.
    Jason: Really?  Who proved that?
    Gilles: I did.

2) Derek: Have you looked at how I do it in MixML?  How do the methods compare?
    Florian: I haven't looked, but I'd be surprised if they are different.  If you do it right, it ends up like this.
   Derek: I was going to say, if you do it right, it ends up like MixML.

Computer security

A British hacker somehow managed to shut down the US Army's computers for 24 hours.
I didn't hear about this.  I thought this comment was interesting.

He had used his own computer with a 56K dial-up modem at his London home with no password protection and somehow managed to evade every security measure the U.S. military had adopted.

70 years seems excessive.  Perhaps the Army should hire this guy rather than put him
in jail. 

Great picture

Haskell 'import qualified'

Haskell's module system is a bit weird.  Consider the following:

import qualified Data.List as L
import qualified Data.Char as L

x = L.concat []
y = L.toUpper 'c'

How can this make sense?  I was interpreting

import qualified Data.List as L

as

structure L = Data.List

in SML.

Apparently the qualified import just makes a new namespace and
dumps all the names from the modules into it.  If there is a conflict,
you simply can't use the name.  For instance, if it was Data.Map and Data.List,
then L.union would be ambiguous.

DMTCP Checkpointing

Checkpointing is the ability to stop a process, save it, and restart it later.  As a user of HOL Light, checkpointing is nearly essential, since every time you start the system it evaluates all of mathematics from scratch.  Loading advanced libraries can take upwards of an hour.  Checkpointing is hard to get right though, and I haven't found a single program that works on the latest Linux kernel.  I started using DMTCP this weekend, and it works perfectly.  I highly recommend it.  The steps are simple.

1) Install DMTCP using a Debian package or from source.
2) dmtcp_checkpoint -n ocaml
3) #use "hol.ml";; (to start HOL Light)
4) dmtcp_command -c (from another terminal.  This checkpoints the process)
5) Kill the ocaml process.  Then do dmtcp_restart on the saved binary.

Works like a charm.

Latex Alert + Array + Infer bug

You can't do the following in Latex:


\documentclass{beamer}
\usepackage{proof}

\begin{document}

\begin{frame}
  \begin{array}{c}
    \alert{\infer{A}{A}}
  \end{array}
\end{frame}

\end{document}

For some reason you can \alert an \infer outside of an \array, but not inside.  Weird bug.

Workaround:  Use tabular instea


\begin{frame}
  \[
  \begin{tabular}{c}
    \alert{\infer{A}{A}}
  \end{tabular}
  \]
\end{frame}

Old Jade and the Zombie!

I'm currently reading

History and Future of Implicit and Inductionless Induction:
Beware the Old Jade and the Zombie!

by Claus-Peter Wirth.  My favorite quote so far:

 In practice, however, refutational completeness by itself does not help in refuting
invalid conjectures or in finding finite proofs for inductively valid formulas.
Only theoreticians completely detached from reality can consider nonterminating
proof attempts in refutationally complete inference systems to be
successful proofs.

Alabama

What is wrong with Alabama?

WTF??

The Senate just passed a bill controlling credit card companies.  What the **** is Tom Coburn thinking?  No wonder people hate Congress.  (Why anyone would need a loaded gun in a national park is a good question, but somewhat beside the point.)

One amendment attached to the Senate bill by Senator Tom Coburn, Republican of Oklahoma, would restore a Bush administration policy allowing loaded guns in national parks. That provision is not in the House version, so there may be discussions between the two chambers over the issue.

BibTeX oddity

Comments don't always work in BibTeX files!  I had the following in my bib file:

@STRING{lncs = {LNCS}}
% @STRING{lncs = {Lecture Notes in Computer Science}}

I wanted the shorter "LNCS" rather than "Lecture Notes in Computer Science".  For some reason, the long form kept showing up in my bibliography.  Transposing the lines gives the desired effect.  Weird...

Designer Clock Puzzle

Guess what's special about this clock.  (Thanks to Florian Rabe for pointing this out.)

Pushcart Prize

I discovered a great short story series in the library, more or less by accident.  It's called
The Pushcart Prize.  The collection I checked out, The Book of Short Stories, contains stories by Tobias Wolff, Tim O'Brian, Mona Simpson and many others.  It's a fantastic collection.

How to give a good talk

Nice lecture on giving good research talks, by Simon Peyton Jones.

Big dog

Quite an amazing video.

http://www.youtube.com/watch?v=W1czBcnX1Ww

Air quality

Great.  Pittsburgh is the worst city for short term particle pollution.  And second worst (behind Bakersfield) for worst long term particle pollution.

A lot of Americans feel comfortable about air pollution, and we often think that it's a problem in a few well-known places, said Dr. Norman H. Edelman, chief medical officer for the American Lung Association....
Pittsburgh topped the list of cities most polluted by short-term exposure to particles. It's still a dangerous city for particulate pollution, pointed out Edelman.

LaTex?

\int_{0}^{1}\frac{x^{4}\left(1-x\right)^{4}}{1+x^{2}}dx

=\frac{22}{7}-\pi

LaTeX Error Message Fail