Invariants should be Unadorned

Properties that always hold, ie: invariants, should not have to be indicated by special notations.  They should be unadorned.  Special notations should only be used to indicate when a property does not always hold.

Lamport's Temporal Logic of Actions violates this principle in that a predicate P holds only in the initial state, and if you want to indicate that it always holds the you have to put a box symbol in front of it:


Similarly, in Daniel Jackson's Micromodularity Mechanism you have to use the keyword 'fact' to indicate that a predicate is invariant.

It seems obvious and natural to me that if a predicate P does not always hold then this should be indicated by an implication Q->P where Q is the condition under which P does hold. 


The Periodic Table by Primo Levi

The Periodic Table is a collection of short stories, some autobiographical, some not, each one associated in some way with a different chemical element.  You might think that this would appear contrived, but it doesn't because Primo Levi weaves most of the stories around his day-to-day life as an industrial chemist in Italy before, during, and after the Second World War.  The impact of Fascism runs as a theme through many of the stories, although only one is directly about Levi's experiences in Auschwitz.  The translation from the Italian by Raymond Rosenthal is smooth and unobtrusive.  The stories are varied and stimulating and I found I could read three or four of them at a sitting without my interest flagging.

Should students of chemistry read this book?  Well, yes, I think they should, but not for the little bit of chemistry they might pick up from it, but because it is a good read and it is part of the cultural heritage of their subject (in the same way that The Double Helix by James Watson is for molecular biology).


Specifications are for Reasoning From

We write specifications of systems in order to be able to reason about those systems.  This reasoning can be formal or informal. It can take the form of proving properties, deriving properties or refining the specification to code.  The purpose of specifications is to allow this reasoning to take place, ie: specifications are for reasoning from.  Looking at specification this way leads me to make the following suggestions:

  • Specifications should be written in a way that makes reasoning easy.  A way to do this is to write them as conjunctions of ready-to-use proof steps, with the pre-conditions and variables of each step clearly visible.
  • Conciseness is not necessarily important in specifications.  Not including irrelevant material is important, as is clearly laying out the relevant material, but using abstruse theories to make the specification as short as possible is not.
  • Graphical notations that have not been designed with reasoning in mind should be avoided.  Just because a notation is graphical does not mean that it makes reasoning easy.

Stargazing by Peter Hill

I only picked up this book because of its title.  I only bought it because, when I opened it, I came across a mention of the island of Pladda.

Back in in the summer of 1972, when I was 13, our family spent three weeks staying with friends on the Isle of Arran.  That holiday was to me rather like what the trip to Corfu was for the young Gerald Durrell in My Family and Other Animals, except that it wasn't wildlife that interested me then, but stars.  Because of the lack of street lamps the skies were darker than any I had seen before and, because of the sea horizon, I could actually see stars further south than I could from back in Cleveland.  And the views of the Milky Way through binoculars were simply breathtaking.  On my return from that holiday I joined the British Astronomical Association and took up variable star observing in earnest. 

Although we were based at Pirnmill, in the north-west corner, we explored all parts of the island, and often from the mountains or from the southern shore-line the islands of Pladda and Ailsa Craig were visible in the distance.  Pladda was small, flat and close in, Ailsa Craig, large, hemispherical, and much further out, down the Firth of Clyde.

In the following summer, that of 1973, Peter Hill, an art student from Dundee, took a holiday job as a lighthouse keeper and spent a few weeks on Pladda and then a few more on Ailsa Craig.  Stargazing is his account of that time, of the characters he worked with, the way of life, and the things that happened to him.  It is an enjoyable, heart-warming read. I am sure that would have lead to hordes of people applying to work as lighthouse keepers, if only the lighthouses hadn't all been automated by now.


Life of Pi by Yann Martel

A very strange book.  The Financial Times reviewer got it spot on when said it is like "Joseph Conrad and Salman Rushdie hallucinating together...".  However, I nearly gave up three quarters of the way through, leaving Pi stuck in the middle of the Pacific Ocean, but I eventually came back to it and followed him through to landfall and beyond.  And I am glad now that I did, even though I did find the ending a little disappointing.  Anyhow, if ever I have to live in close quarters with a Bengal tiger, I now know what I have to do.