[ This is a brain dump of a bunch of topics collected over the weekend; I also saw a performance of Purcell's Dido and Aeneas, so that's why it's a potpourri and not something more structured. Call me back when I've had more coffee, later in the week. ]

From a research perspective: wow! a verified microkernel. I left my formal verification stuff behind at the university (which reminds me I still have a desk to partly clean out and an HP9000 to trash), but the idea of verifying a Haskell program isn't all that terrifying; getting the Haskell-C mapping and the machine model mapping right and validated is something to lose sleep over, though. Something to occupy a bunch of grad students for a long long time. So hats off to the UNSW for getting it done and also for writing a wonderfully concise and witty FAQ.

There's a little bit on tax money going to waste, this time around a CMS for Birmingham; given the importance of the specification for l4v (above) one would think that the specs for a CMS would be somewhat hammered out by now -- certainly as far as character encodings go. I'm not sure I agree with the middle of the article, though, where it goes (in hindsight): well, we could have just used Wordpress, right? Much as I like Wordpress (it runs the FSFE blogs, and although it isn't entirely compatible with Konqueror 4.2.2, it does well enough) I don't think it's the solution to every CMS problem. There could well be additional hidden requirements that the article glosses over and that would have mandated a custom solution.

Still, it's government money, and I do believe that a custom solution funded by government should be Free Software afterwards, as it represents an investment by society as a whole to improve its infrastructure.

Baptisterium

On Free Software topics, I ran across Why Code For Free? on LinuxPlanet; I'm actually none too happy about that article. It has a lot of woolly thinking in it. It's 2009, come on, couldn't we at least get a characterization of the four freedoms that the GPL aims to protect that is both concise and gripping? Let's not forget, rhetoric (the modern trend of invading, tracking, and trying to control personal use) aside, that freedom 0 is only very very rarely touched upon by any license [mental exercise: if software is delivered without warranty or claim of fitness for a particular purpose, can you add restrictions stating that it is unfit for some purpose or may not be used for some purpose?]. In retrospect, I suppose that the end of the introduction (non-coder, us lowly end users) should have tipped me off that this is hardly a piece to take seriously.

K-Logo mosaic

David Jarvie is the KDE "date and time dude". Give him a good long scarf and I'm sure he could figure in Dr. Who. My hat off to anyone who deals with timezones and calendar systems on a daily basis. While tooling around on the topic, I found some interesting definitions of the epoch (an arbitrary moment to start counting time from), a leap back and a more recent reintroduction of the leap back. This time related to standardization and arbitrary kludges in calendars (man -s 1 cal ; cal 9 1752). David, next Akademy you get more beer.

Lastly, I recently took a look at a reconstructed 4th century baptisterium, where I found the K-logo in the mosaic in the floor. So I think that expands the range of dates KOrganizer -- and KDateTime -- should support easily by a great deal. After all, St. Augustine had appointments too.