Formal Methods

I don't understand formal methods. A group has claimed to have formally verified the L4 kernel. What does this mean? I suppose that this means that specification of the kernel has been written as a mathematical proof. Then it must have been demonstrated that the C code exactly matched the proof.

But if it's easier to write the specification than the code, that must mean that the programming language isn't very good. And yes! This is borne out by the sort of programming errors that are found when comparing the specification to the implementation:
  • Buffer overflows
  • Null pointer dereferences
  • Pointer errors in general
  • Memory leaks
  • Arithmetic overflows and exceptions
These are mostly solved by using a decent programming language such as Python.

Ben Laurie talks about this in his post on formal methods.



Like many others, I read Paul Graham's Lisp essays and thought I should give Lisp a go. I installed Clojure and wrote my first Lisp program:

(defn num_books
(num_books dist 0 0))
([dist achieved nbooks]
(>= achieved dist)
(num_books dist
(+ achieved
(/ 1
(+ nbooks 2)))
(+ nbooks 1)))))

(println (num_books 1.5))

If you put a book on the edge of a table you can balance it so that it sticks out half a book length. Place another judiciously on top and it'll stick out 1/2 + 1/3 book lengths. You give the function above a number of book lengths you want the stack to stick out, and it'll return the number of books you need.

Coming from a Python background, wouldn't it make sense to use whitespace instead of parentheses?

defn num_books
num_books dist 0 0
[dist achieved nbooks]
>= achieved dist
num_books dist
+ achieved
/ 1
+ nbooks 2
+ nbooks 1

num_books desired_distance

Also, I'm interested to compare this function with its Python equivalent:

def num_books(desired):
achieved = 0
nbooks = 0
while achieved < desired:
achieved = achieved + 1 / (nbooks + 2)
nbooks = nbooks + 1
return nbooks
The Python one is shorter, how can this be? Okay a re-write of the Lisp version:
(defn num_books
(loop [nbooks 0 achieved 0]
(< achieved dist)
(inc nbooks)
(+ achieved
(/ 1
(+ nbooks 2))))

Python 166 chars, Lisp 186 characters. What am I doing wrong?


Where Angels Fear To Tread

Here's a painting of E.M.Forster. Note that his head is pointy at the back. This is believed to be source of his literary powers.

I was in a cafe and someone there recommended Forster, so I got Where Angels Fear To Tread from the library. It was his first novel, written when he was 26. I think this shows, in that he is careful to demonstrate his cleverness. He also deliberately uses terse, modern language, wanting to be fresh and free of pomposity. The economy of expression is a sign that he is afraid of losing the reader's attention. More experienced writers are less constrained and are a bit more expansive. For instance, in The Brothers Karamazov, Dostoevsky uses seemingly redundant verbiage with abandon, yet his genius is that this has meaning in itself, and so is not wasted.

Thank you Forster, this is a very thoughtful book.


Dell: Get the standard Ubuntu working

While I'm in the mood for sounding off, I'm not entirely pleased with Dell's behaviour. Janos at work bought a Dell Inspiron Mini 10v.
It comes with Ubuntu installed, but it's not the standard Ubuntu distribution, it's been tinkered with by Dell, mostly for the worse Janos found. So he installed the latest version of Ubuntu. This meant that the wireless network card didn't work. And here's my message to Dell:
  • Always use the standard Ubuntu distribution.
  • If the standard distro doesn't run, work with Ubuntu to fix the problem.
Luckily, Janos is interested in computers and managed to get it working. But as he says, this won't do for the average user.

I don't want to overstate the problem, I run two Dell laptops with Ubuntu, and they work really well. Much better than Windows! I'm really pleased Dell is giving users the choice.

Directed Identity

I read Glyn Moody's writings with interest, but with his post Why Single Sign On Systems Are Bad I think he's made a rare slip. Here's a note to Glyn on why I think he's wrong on this occasion:

You conflate single sign-on (SSO) and single identity. OpenId lets you have SSO and lets you have a separate identity for each web site you visit. It's called Directed Identity, and Peter Williams gives a good explanation of it.

Yahoo! implement directed identity. Anyone with a Yahoo! account that signs in to websites using OpenId automatically has a different ID for each web site. When you sign in to the web site you just type yahoo.com in the OpenId box, and Yahoo! magically works it all out.

I got that last paragraph wrong. As Will Norris explains, Yahoo! implements identifier select and can give an opaque URL, Yahoo! does not support directed identity. Google does support directed identity.