The Economics of Colonizing Other Planets

Anthropologist John Hawks has produced what I regard as the definitive refutation of  Stephen Hawking's argument that humans ought to spread to other planets in order to survive catastrophes that strike Earth.  His refutation is based on economic and genetic considerations.

Lisp as an 'Improved XML'

Steve Yegge's old blog, Stevey's Drunken Blog Rants, contains a lot of good reading for anyone interested in programming.  I particularly like his post The Emacs Problem in which he demonstates convincingly that the ancient programming language Lisp is better at representing structured text than the currently fashionable XML.  Here is a sample Java error log in XML:

<?xml version="1.0" encoding="utf-8" standalone="no"?>
 <!DOCTYPE log SYSTEM "logger.dtd">
 <log>
 <record>
   <date>2005-02-21T18:57:39</date>
   <millis>1109041059800</millis>
   <sequence>1</sequence>
   <logger></logger>
   <level>SEVERE</level>
   <class>java.util.logging.LogManager$RootLogger</class>
   <method>log</method>
   <thread>10</thread>
   <message>A very very bad thing has happened!</message>
   <exception>
     <message>java.lang.Exception</message>
     <frame>
       <class>logtest</class>
       <method>main</method>
       <line>30</line>
     </frame>
   </exception>
 </record>
 </log> 

And here is the same in Lisp:

(log
 '(record
   (date "2005-02-21T18:57:39")
   (millis 1109041059800)
   (sequence 1)
   (logger nil)
   (level 'SEVERE)
   (class "java.util.logging.LogManager$RootLogger")
   (method 'log)
   (thread 10)
   (message "A very very bad thing has happened!")
   (exception
     (message "java.lang.Exception")
     (frame
       (class "logtest")
       (method 'main)
       (line 30)))))
 

Not only is the Lisp version shorter, less verbose and clearer, it also doesn't require you to learn another half dozen half-baked programming languages and frameworks in order to be able to write a program to read it and process it.

The older I get, the less patience I seem to have with unnecessary syntactic baggage, and more attractive I find Lisp's simplicity.  However, for the time being I think I will stick with Haskell.

A New Version of Alloy

Beta versions of version 4 of the Alloy Analyzer are available from here.  This version includes some changes to the syntax of the Alloy language (see here), which is unfortunate since it makes Daniel Jackson's new book obsolete only 6 months after it was published.  However, updating models from version 3 to version 4 syntax does seem to be fairly easy. Still, it might be a good idea to have Alloy 3 and Alloy 4 installed alongside each other, at least until you have got used to the new version.

Never Let Me Go by Kazuo Ishiguro

A strange and moving story. Thirty-one year old Kathy H. looks back over her life to her days at Hailsham school and tries to make sense of it.  Initially Hailsham seems like a typical boarding school but gradually the reader becomes aware that the world it exists in has a dark secret, the full nature of which is not revealed till the penultimate chapter.  Mallory Towers meets 1984 is how you might describe it, though Ishiguro is a much better writer than both Blyton or Orwell.  When reading Ishiguro I  continually find myself struck by the power of writing: how a string of simple words describing the lives of ordinairy people can produce such a gripping experience.

The Role of Proof in Software Development

Many software developers seem to think of proof as a of a sort of mathematical bludgeon that is used to intimidate people into accepting that a piece of software is correct. However, I see proof more as an explicit statement of the reasoning and assumptions that went into the construction of the software.  I see constructing a proof as more a way of exploring the problem and detecting errors than a way of convincing others.