It’s pretty common for database-driven apps to display a “last updated” field. For instance, here is a screenshot of my Mail app on my iPhone, showing that my emails were “Updated Just Now”.


And here is a screenshot from the RealTimeTrains app, showing that the information was “Updated a few seconds ago”.

photo 2

Why do apps insist on using relative timestamps like this? It’s all very well having a piece of text to say that the information was “just updated”, but how do I know that the piece of text itself is up-to-date?

(It’s a bit like those “Lost Cat” posters that say “missing since last Friday” and are then left up for months.)

If instead the text gave an absolute timestamp like “Updated at 07:57”, then I would know that the information is up to date, and that the app hasn’t simply gotten stuck.

I transcribed Barry Gray’s theme song from Stingray, Aqua Marina, into piano sheet music. There’s a vocal part, replete with lyrics, plus a keyboard part comprising a right-hand and chord symbols. It roughly corresponds to what you might find in a musician’s “fake book”.

Available as a pdf file, as an editable Noteworthy Composer file, and an mp3 audio file (recorded on my iPhone).


Here are some tips for travelling from Cambridge to London. Prices fairly accurate in April 2015.

By coach

National Express operates a service between Cambridge and London. It’s not a well-used service, chiefly because it takes a good two and a half hours. However, note that if you don’t go all the way to Victoria but instead jump onto the Underground network at, say, Mile End, you can slice off the last hour or so. It’s also worth noting that 10-trip tickets are available (only from the driver). These work out as £5.65 for each one-way journey, so they are cheaper (and quicker) than buying advance tickets online, but they do not guarantee a seat (not that getting a seat has ever posed a problem for me).

By train

Consider taking the train to Liverpool Street (LST) rather than the default King’s Cross (KGX). There are “slow” and “fast” trains to both destinations, with the fast LST trains taking about 70 mins compared to the fast KGX trains taking about 50 mins. Although the LST route is a little slower, it has a number of advantages. First, it is much less crowded. Second, it is noticeably cheaper: if you travel with a Network Railcard after 10am, you can get an day return (which includes a Zone 1-6 London Travelcard, and has no evening peak restrictions) for £16.75; the same journey to KGX costs £20.80 (with Travelcard) and you cannot return between 1630 and 1900. Both the LST and KGX routes use trains of varying quality; the LST route has both the best trains and the worst. Those providing the 1004 and 1021 service to LST, and the 1707, 1737 and 1807 services back to Cambridge, are the best trains, replete with large tables, comfortable seats, and free (if rather intermittent) wifi.

Oh no

When designing the English character set, it was quite a bad idea to make the letter O (“oh”) look so similar to the number 0 (zero).

But what turned a bad situation into an absolute disaster was the introduction of the convention of pronouncing the number 0 as “oh” – as in “double-oh seven”, or the freephone number “oh eight-hundred”. At least if the convention had been to pronounce the number 4 as “dee”, one could potentially resolve the ambiguity by looking at the shape of the character. As things are, a vertically-stretched circle called “oh” can equally refer to the 15th letter of the alphabet or to the number zero.

Sentient beings can often infer whether a given ovoid is intended as a number or a letter from its context. But computers cannot, and in an increasingly computerised world, this is an increasing problem. A phone number entered as O800 123 456 can be succesfully interpreted by a human, but an unthinking machine will reject it as invalid. My friend who thought, for many years, that his postcode was “DE3 OAB” until I pointed out to him that the third character from the end had to be a number, had no trouble receiving mail handled by human operators, but would have struggled to resolve his delivery address on Amazon.

Here’s another tricky area: car registration numbers. Cars built between 1983 and 2001, are identified by a 6- or 7-character sequence comprising a letter, followed by two or three numbers, followed by three further letters. Those built more recently are identified by a 7-character sequence of two letters, two numbers, and three letters. Bearing in mind that the font in which these characters are printed does not clearly distinguish zeroes from ohs, it is quite impossible to judge whether car FO12ABC is 27 years old or just 3 years old. Unless the car is in front of you, that is.

And it’s not just zero and oh that can cause alphanumerical confusion. The uppercase letter I (“aye”) looks suspiciously similar to the number 1 (one), and to the lowercase l (“ell”). In fact, legend has it that the Queen utters sentences like “One would like to watch telly now” simply because she misread the “I” for a “1” a long time ago and has continued the habit ever since.

Here are several really useful free Mac apps that I’ve come across recently:

  • Macfusion (free). Lets you mount remote filesystems over SSH or FTP, and access them through Finder. Far nicer than using the ssh command in Terminal, or a third-party FTP client. Depends on OSXFUSE. Notes:
    • Finder does already provide FTP access (via “Connect to server…”), but it’s read-only.
    • In order to have write access over SSH, you’ll need to do the trick described here to map your local username to the username of your SSH account.
    • I find it convenient to place a link to in Finder’s toolbar.
  • BetterTouchTool (free). Brings to Mac the excellent ‘aero-snap’ feature of Windows 7 (plus a few other nice features).
  • Spark (free). Lets you assign custom keyboard shortcuts. Really stable and powerful. Doesn’t look to have been updated for a couple of years, but still works fine on Snow Leopard.
  • VirtualBox (free). Run Windows or Linux on your Mac – and no need to dual boot. I’m staggered by how well this works.
  • BibDesk (free). I use this to manage my PDF library. Very powerful and customisable.
  • PDFNut (free). A PDF viewer with Chrome-style tabs. I only started using it yesterday, and I love it already.

In a recent research paper, I formalised some of my theorems in the proof assistant Isabelle, but left some of them as just proved ‘by hand’. I found it helpful to use a different ‘QED’ symbol depending on which method I had used.

Below is an enlarged version of the ‘three cubes’ symbol in the snippet above, together with the original Isabelle logo for comparison. The new symbol is designed to be suitable for black-and-white printing at a small size, and can be generated by the LaTeX code given below.


\begin{tikzpicture}[x=0.8mm, y=0.8mm, 
     baseline=-0.3mm, line join=round]
 \draw (0,0) rectangle +(1,1);
 \draw (2,1) rectangle +(1,1);
 \draw (1,2) rectangle +(1,1);
 \filldraw (1,-1) rectangle +(1,1);
 \filldraw (3,-2) rectangle +(1,1);
 \filldraw (2,0) rectangle +(1,1);
 \draw (1,0) rectangle +(1,1);
 \draw (2,-1) rectangle +(1,1);
 \draw (3,1) rectangle +(1,1);


One could even go a step further, and extend this idea into a potential new logo for Isabelle.

New Isabelle logo

The picture above is generated by the following LaTeX code.

\begin{tikzpicture}[x=4mm, y=4mm, baseline=6mm, 
     line join=round, draw=black]
\begin{scope}[every node/.append style={yslant=-0.5}, yslant=-0.5]
 \filldraw[fill=blue!25] (0,0) rectangle +(1,1); 
 \node at (0.5,0.5) {$\lambda$};
 \filldraw[fill=blue!25] (2,1) rectangle +(1,1); 
 \node at (2.5,1.5) {$=$};
 \filldraw[fill=yellow!25] (1,2) rectangle +(1,1); 
 \node at (1.5,2.5) {$\vdash$};
 \filldraw[fill=red!25] (4,2) rectangle +(1,1); 
 \node at (4.5,2.5) {$\alpha$};
 \filldraw[fill=red!25] (3,3) rectangle +(1,1); 
 \node at (3.5,3.5) {$\rightarrow$};
 \filldraw[fill=yellow!25] (2,4) rectangle +(1,1); 
 \node at (2.5,4.5) {$\forall$};
 \filldraw[fill=black!25!blue] (1,-1) rectangle +(1,1);
 \filldraw[fill=black!25!blue] (3,-2) rectangle +(1,1);
 \filldraw[fill=black!25!yellow] (2,0) rectangle +(1,1);
 \filldraw[fill=black!25!yellow] (3,1) rectangle +(1,1);
 \filldraw[fill=black!25!red] (4,-1) rectangle +(1,1);
 \filldraw[fill=black!25!red] (5,-3) rectangle +(1,1);
 \filldraw[fill=blue] (1,0) rectangle +(1,1);
 \filldraw[fill=blue] (2,-1) rectangle +(1,1);
 \filldraw[fill=yellow] (3,1) rectangle +(1,1);
 \filldraw[fill=yellow] (5,2) rectangle +(1,1);
 \filldraw[fill=red] (4,0) rectangle +(1,1);
 \filldraw[fill=red] (3,-2) rectangle +(1,1);
\end{tikzpicture}\hspace{4mm}{\Huge\bf Isabelle}

He has feet the size of rabbits.
He has feet the size of rabbits’.


Get every new post delivered to your Inbox.