corollary: Computer Science

Wednesday, 21 March 2012

The Scary Bit of the Scala Experience

Listening to:

Goodbye Pork Pie Hat from Charles Mingus’s Mingus Ah Um

Scala is Wonderful, But

Despite being another of those worrying single-implementation languages (see also: Perl, OCaml and Haskell), Scala may just be a language I could use instead of SML. It certainly has a number of advantages compared to SML. Firstly, and most importantly, it still seems to be under development, and has thereby managed to attract a community of keen users. (In the SML world, only Poly/ML seems to get any development love.)

It also supposedly gets to leverage the big wide world of Java code, which is pretty appealing. I haven’t confirmed that this is actually possible without undue pain, but being able to link against arbitrary other bits of Java would be pretty awesome. After all, there’s a heck of a lot of Java out there (some of which is presumably useful).

Of course, compiling to the JVM means that you get reasonable portability “for free”, but I think it’s more important that it also gives you consistent access to proper concurrency on multi-processor systems.

(I don’t want to suggest other options might not be awesome too. In particular, Haskell is clearly pretty amazing and my limited experience of writing xmonad configuration files has helped me remain impressed by it.)

Scala’s biggest disadvantage seems to be the build system. That whole Java eco-system is a mysterious world to me, but it seems to have thrown away the simplicity of make and replaced it with the horror of sbt (itself built on top of something called maven apparently). I can build stuff with sbt: I type sbt compile and errors get reported, but I dislike having the system be such a black box. I know how make works, and knowing how it works means I can build a good mental model of what is happening when I invoke it. With sbt I might as well be praying to an inscrutable deity.

Perhaps I just have to invest the time in learning its intricacies.

Wednesday, 15 February 2012

Abstract Algebra in HOL4

Listening to:

Mahler, symphony no. 1, “Titan”; Royal Concertgebouw Orchestra, conducted by Leonard Bernstein.

By algebra I mean stuff like group theory. This has always been difficult in HOL, mostly because of the relative inexpressiveness of its simple type theory. In particular, there’s no good way to set up a type of all possible groups, which is the natural thing to want. The best thing possible would be to get a type of groups over a parameter corresponding to the type of the carrier set. In other words, you could set up a type operator group of arity one, so that the type α group would be the set of all possible groups with carrier sets that have elements from the type α.

The funny thing is that most people don't seem to do this. Instead, they work with what you might call a pre-group. Such a thing might be a triple of carrier set, group operation, and group identity. Not all such triples are really groups because the required group axioms may not be satisfied.

The standard approach is to then define a predicate isGroup over the pre-groups. Then isGroup(pg) is true when the pre-group pg does satisfy the appropriate group axioms. You might then manage to prove a bunch of theorems of the form

  ⊢ isGroup(g) ∧ xg.carrier ⟹ g.plus g.identity x = x

You can do a whole lot of group theory this way, but just about every theorem you ever prove is going to have a isGroup pre-condition of some form. The experiment I want to perform is taking the subset of pre-groups corresponding to those triples that really are groups, and to then define a genuine HOL type on that basis.

You might still get theorems that require elements to be members of the underlying carrier set, but it’d still be an improvement, I reckon. Nor can I really see a possible down-side, at least as far as groups are concerned.

The only fiddle necessary is when you move on to rings and fields where the algebraic structure is usually understood to contain at least two elements (the zero and the one). You can’t then construct such a structure uniformly for all possible carrier types in HOL, because types may only contain one element. There are two possible work-arounds:

  • Make the carrier type actually be α option or some such, so that you can be sure that the type really is always big enough. This is pretty ick really.
  • Allow rings and fields to have zeroes and ones that are the same. I don’t know at this point how much violence this would do to the general theory.

Better yet, I have a potential student ready to start doing just this experiment, so I may be able to report back shortly.

Thursday, 16 June 2011

Bitcoin

Listening to:

Beeps and bells from the iPad game being played next to me.

Monday, 9 May 2011

Github (and git) for HOL4 development?

Listening to:

Mahler, symphony no. 9. Pierre Boulez conducting the Chicago Symphony Orchestra.

Version Control Systems

I’m beginning to think that we should move HOL4 off Subversion and onto git, preferably hosted on github.com. Here’s why:

  • Most importantly, git makes dealing with a certain class of contributor easier. Currently, the Subversion at SourceForge setup means that we can only support two sorts of developer: the regular developer that is allowed to make arbitrary commits across the whole source-tree; and the very occasional developer who mails a regular developer a patch. The regular developer makes the commit themselves, perhaps adding that the bug-fix, additional theory or whatever came from the very occasional developer.

    With git, we can have an intermediate class of developer, the occasional developer. These people can establish their own forks of the source-code, do their own stuff with it, and then make pull requests. If their commits do get incorporated into the “official” repository, their names will still be attached to the commit objects.

  • An advantage of moving to github specifically is that it allows us (through “beta” software admittedly) to view a git repository as a Subversion one, meaning that existing HOL4 developers who don’t want to have to learn git can continue to make commits using the svn command-line tool, in a way that will remain familiar.

    This facility at github is described (in rather sketchy fashion) here.

  • The last advantage is that git is just much cooler than Subversion in many ways. In particular, it gives developers good support for branching and merging, with complete local copies of repositories.

Possible disadvantages:

  • The support for Subversion as a git client at github may not be robust.

  • Our big existing Subversion branch (HOLω; see here) may prove difficult to graft onto the git repository in a nice way.

    My guess at the moment is that we could checkout master, dump the HOLω branch on top of that and do a fresh commit. In that way, we would encapsulate all of the existing history in one huge commit. The subsequent development of HOLω on that branch could use git’s good support for cherry-picking and merging in general to pull across new stuff from master.

Thursday, 28 April 2011

Emacs and its fonts

Listening to:

Schutz, Sinfonia Sacrae, op. 6, no. 8: Adjuro vos Filiae Jerusalem

Emacs has terrible font handling: there seem to be about three different APIs, and the documentation doesn’t seem to be as clear as it might about which to use. Then there is the additional confusion to do with fonts on X. There are old style fonts that are specified like

  -foo-bar-medium-104-42-*-wooble-*-*-*-

and then there are GTK font specifications like

  Deja Vu Sans Mono 

sometimes with additional -12 type suffixes.

It’s all terribly confusing. I recently found myself unable to set my font to one that was narrow enough to allow two Emacs windows across one 1280 pixel wide monitor. I posted to Stack Overflow about it, but nobody has come to my aid just yet.

In the meantime, I have adopted a 9pt Lucida Typewriter Sans that looks OK. This does produce a pretty narrow Emacs window, and when I switch to xmonad, I’ll be able to have two such windows tiling nicely beside each other.

Thursday, 14 April 2011

A Theorem-Proving Exercise for Novices

Listening to:

Louis Armstrong, Ain’t Misbehavin’.

Sub-lists

I have used this exercise as a good one for getting a student up to speed with a proof-assistant such as HOL4.

Using your theorem-proving system of choice, define the notion of sublist, a binary relation on lists l1 and l2, which is true if and only if all the elements of l1 appear in l2 in the same order. Naturally, l2 may contain other elements.

For example, [1,2,3] is a sub-list of [0,1,2,2,4,5,6,3,10], but is not a sub-list of [1,4,3,2].

Having defined this relation in whatever way seems most natural, prove that it is reflexive, anti-symmetric and transitive.

Sunday, 7 December 2008

It’s a wonder computers ever work

Listening to:

The whir of a Macbook Pro’s optical drive.

God I hate computers

I am attempting to install Windows on a partition of my Macbook Pro laptop. It’s turning into a real hair-pulling-out experience. My current task is to burn a copy of my Windows installation disk, because some opinion on the web has it that the optical drive doesn’t read Microsoft’s media very well. (This did seem to be the case just attempting to read the README files on the disk.)

But now I have a disk image ready to burn, and the drive is having fits over the blank CDROM I just put in it. I’ll try a blank DVD instead. That’s better I think: I guess my drive is getting picky about everything it’s doing. (And don’t get me started on getting Macs to eject things.)

With a disc it’s burnt itself, I’m hoping that the Windows installation process won’t get its knickers in such a knot.

But! What has really been exercising me is the general inadequacy of the Web as a reference vehicle. If you do a Google search on your problem, you will in all likelihood be led into a deep thicket of web-fora. If only the Web had somehow kept Usenet alive, so that there would be one good source for all this sort of discussion instead of zillions of little ones. In this brave new world, one just has to hope that Google’s algorithms for assessing the worth of the pages it finds are up to scratch and taking you to web-pages with answers that aren’t completely bogus.

My new disk image is just about burnt, so I will bring this entry to a close and cross fingers, toes and any other extremities I can find.

Tuesday, 29 July 2008

Privacy is such an out-moded concept

Listening to:

Bach, Duet in F major, BWV 803, played by Christine Jaccottet.

An argument for NoScript

If you go to this site, you can push a button that gets the site to analyse your browsing history, and then, using some simple statistics on web-site visitor patterns, determine your likely gender.

I had an 89% chance of being male.

You might feel justifiably concerned that your browser was willing to cough up this information. In particular, a remote site could extract this information without requiring you to first push a button. The information probably isn’t linked to you directly because we assume that the browser is only providing history and not any other details. However, if you’ve just signed up to a site with an e-mail address, then there is a link for free.

This leads me to recommend the NoScript extension for Firefox. This gives you much better control of the JavaScript that may or may not be running on your computer.

Tuesday, 4 December 2007

Overheard on IRC

Listening to:

Bach, Fantasia and Fugue in C minor, BWV 537, played by Peter Hurford.

Why is it only now, when I come to write the slides, that I realise how weak some of the things we’re proving are?

Monday, 2 July 2007

Formalisation and Specification

Listening to:

Mozart, Divertimento in B flat, K.99. Played by the Vienna Mozart Ensemble, led by Boskovsky.

Dijsktra Making Good Sense

And if you have not a ready-made function [...] at your disposal in terms of which to describe the net effect of such a compound statement, invent this function and be sure that its properties are nice and also the ones that you want. If you cannot find such a function, don’t ignore that warning, for then you are on the verge of messing things up.

From EWD-273 by Edsger Dijkstra.

(Perhaps I’m going to turn this weblog into my commonplace book, though I do want to get back to the backlog of book reviews...)

Friday, 9 March 2007

Detecting human-level intelligence

Listening to:

I wants to stay here, from Cole Porter’s Porgy and Bess. Sung by Ella Fitzgerald.

Way Cool Factor 10, Mr. Sulu

I was dead-impressed with this cool test for detecting human-level intelligence, by getting people to tell the difference between photos of cats and dogs. This is something that machines can’t do very well, if at all, but something that a child can manage with high levels of accuracy from a young age.

And when the machine learning gurus get their systems up to the task of telling cats from dogs, perhaps they will founder on judging whether or not people are attractive. That’s the premise behind hotcaptcha.com. There are two obvious problems with this latter though: it seems likely that a fair component of beauty is culturally determined, and once you take that out, maybe the rest is determined by “simply” assessed numbers like amount of flesh on display coupled with symmetrical faces...

Friday, 15 September 2006

Being spied on by bill-boards

Listening to:

Bach, St. Matthew Passion.

Biting the hand that feeds me

Just saw this publicity material for a NICTA project. It sounds very swish technologically, but I do find the prospect of being observed by cameras attached to bill-boards a little disturbing, even if all they’re doing (indeed, all they’re currently capable of doing) is trying to determine if I’m looking at the bill-board and for how long.

Monday, 11 September 2006

Higher-order functions win the day!

Listening to:

Chopin, 24 Preludes, op. 28. Played by Jorge Bolet (Decca 448 985-2).

Parsing C is a pain, but higher-order functions are great

I’ve recently spent quite a bit of time re-writing a C parser for work. C is a pretty simple language in many ways, but one of its decided obscurities is its syntax for declaring variables. In a language that does this straightforwardly (like Pascal or SML), you can write things like

   x : int

to mean that the variable x is of integer type. The syntax is simple: a variable name, followed by a colon, followed by a type.

Superficially, C looks as simple. To do the analogous declaration, you write

   int x;

The rule looks simple: type first, and then variable name, with a final semi-colon. But this is not the rule at all! To say that x is an array of 10 integers, you write

   int x[10];

The syntax [10], for indicating that the type is an array, is associated with the variable name, not the base type. You might also wonder what

   int x[10][5];

means. Is it five arrays of length ten, or the other way round? (It’s ten arrays of length five.)

Further, in many situations you can declare many variables at once, by separating them with commas. For example,

   int x,y,z;

declares three variables, x, y and z and says that they all have integer type. Now, if you write

   int x[10], y;

the “array of 10 elements” modifier applies to just the x, so that y is just of type int.

Then there are pointers. To say that variable x is of type “pointer to integer”, you write

   int *x;

So, given all that, you might like to have a guess as to what the following declares:

   int *x[10];

Given all I’ve told you so far, you can’t know, because you have no way of telling if the array bit of the declaration is at a higher level than the pointer bit. In fact, it is the array bit, so that it means that x is an array of ten pointers to integers. If you wanted a pointer to an array of ten integers, you’d have to write:

   int (*x)[10];

What does this all have to do with higher-order functions? Well, the natural thing to do when parsing C is to generate values for each syntactic form. Here the interesting forms are the declarators, which include pointer, array and variable name information. A declarator is really a function: if you give it a type, then it builds that type into a bigger, more complicated thing. The empty declarator (which you get if you just have a bare variable name) is the identity function: the type you put in is the type you get out. (The types that we’re putting in come from the type that occurs to the left. In the examples above, this has always been int, but it could be char, float or any other C type.)

The higher-order-ness arises when you think about what the square brackets used for arrays must indicate. The basic situtation is that you have some other declarator (d), followed by the square brackets containing an array size, ten say. The grammar production looks like:

declarator ← declarator[integer]

So d is itself a function, and we have to calculate a new function to be the value of the whole thing. In other words, we have a higher-order function: one that takes as parameter a function. If d takes τ to d(τ), then our new function has to take τ to d(τ10), where I have used super-scripting to indicate the array type. I.e., τ10 is an array of 10 elements of type τ.

We can see this in an example. If the syntax is

   int x[10][5];

then the innermost d function takes a τ to τ10. By appending the [5] syntax, we construct the type function that takes a τ to 5)10, ten repetitions of a five-element array, and not the other way ’round.

The case of the pointer syntax is similar. The syntax looks like

declarator ← *declarator

and if you have a function d corresponding to the declarator following the *, then the new function should take a type τ to d(ptr(τ)). Thus the syntax

   *x[10]

which the precedence rules tell us should be viewed as *(x[10]), first generates the function for the array, which takes τ to τ10. Then this is combined with the pointer notation, to give a function which takes τ to (ptr(τ))10.

Friday, 25 August 2006

Electronic voting

Listening to:

Schönberg, Verklarte Nacht.

At FLoC...

I was at the FLoC 2006 conference over the last ten days or so. While there I saw David Dill give an invited talk about electronic voting. I was struck by the analogy he drew to describe almost all current electronic systems.

When using an electronic system, it is as if one goes into a voting booth to find that one has to dictate one’s votes to a man behind a curtain who says he will fill out and deposit your vote in the ballot box, but that you will not see any of this happening.

No matter how much faith you might have in the implementors of the system to have implemented it correctly, and to have defended it against possible attacks (i.e., no matter how much faith you may have in the man behind the curtain), such a system fails to be transparent. And transparency is the great virtue of traditional paper systems: everyone gets to see the democratic algorithm in action at all of its stages, and to check that it is being performed correctly.

Friday, 10 June 2005

Router magic

Listening to:

Debussy, string quartet. (His only one I guess.)

Hi-tech wizardry

I’m writing this on my lap-top, sitting in the lounge, and connected to the web wirelessly. Yes, all this is possible with modern technology. We bought a router over the weekend, and now we have two computers wired to it with ethernet cables, as well as the wireless connection to the laptop, when it’s at home. This feels pretty cool.

Of course, the lap-top generates far too much heat to be left on my lap for very long, even through denim jeans. (I will be turning it all off once I’ve done this.) In other “technology is not always quite so perfect” news, I think I have forgotten my Firefox master password on the laptop. I don’t have much protected by it, so I’ve tried to reset it. But it’s not clear to me that I’ve even managed to do this. Sigh...

Thursday, 21 April 2005

Keeping it simple

Listening to:

Dinah Washington singing I could write a book.

The KISS principle in software

A group of us from my building regularly go to lunch together. For a while, the practice was for someone to wander ’round the building, knocking on people’s doors and saying “Lunch?” With up to about 10 people to check on, this was tedious. Further, I often seemed to be the person that broke first and started the process.

So I called, loud and tediously long, for a software solution to our problem. (I wasn’t volunteering to implement it, but had plenty of ideas on what the solution should look like.) Someone did volunteer to do it, and within just a few days (he did have a real job to do at the same time), we had a system that has proved to do all we need, and which is also appealingly simple.

People who want to be part of the lunch-group run a little client on their computers. It appears as a little sandwich logo. Then, at any point after 12:00, anyone can push the logo and cause their sandwich to start flipping (from right way up to upside down and back again). Simultaneously, the client sends a message to the server, which does nothing more than forward the message to all of the other clients (which register with the server when they start up). When a client receives a message, it also starts flashing.

And that’s it—there’s absolutely no state in the server.

There are all sorts of potential problems with this solution, but the point is that it achieves exactly what it set out to do. Having a little icon flashing in the corner of your screen is supremely distracting, so there’s no danger of missing the message. People understand exactly what the message means, and can choose to assemble outside the building for the trip to lunch, or not, as the fancy takes them.

Sunday, 31 October 2004

ユーニコードの世界が凄い

Listening to:

Stan Getz and Joao Gilberto, Corcovado.

The Japanese in my title literally means “The world of Unicode is wonderful”, which I decided was the idiomatic way of getting “The wonderful world of Unicode”. I’m impressed with it at the moment because I was recently browsing the Wikipedia article on Al-Khwarizmi, which has the Arabic form of his name (أبو عبدالله محمد بن موسى الخوارزمي). I cut and pasted the Arabic into a presentation I’m writing with Open Office’s PowerPoint equivalent (ooimpress), and found it transferred perfectly. Based on the funny things my cursor was doing, I think ooimpress also knew that this was a right-to-left text.

I was sore amazed.

On the other hand, writing my Japanese title was quite tedious. For one thing I decided to use HTML numeric entities, so my title in the raw actually looks like ユー... which is pretty cryptic. (Wikipedia has done the same thing with its Arabic.) Using Unicode charts to find all of the various characters one-by-one is also a very tedious way of working. Jamie’s set up the server here to serve UTF-8, so I could use the “real” characters directly, except that I don’t have an editor that could cope, and I’m not sure that Movable Type’s text entry boxes would cope either.

Of course, if you find your browser turns all of my foreign characters into strange gibberish, you should probably get rid of it, and find a more modern alternative. Alternatively, your fonts may need updating.

Wednesday, 14 January 2004

Our very own Y2K bug

Listening to:

Schumann, Piano trio in D minor, op. 63.

A time overflow bug in Moscow ML

Some time on 10 January, 230 seconds had elapsed since midnight on 1 January, 1970.

Deep in HOL’s dark internals, there’s code that calls the ML function Time.now(). This function returns the current time in the form of an opaque type that you can only manipulate using the functions defined in the Time API. One such function is Time.toSeconds, which turns a time value into an integral number of seconds since 1 January 1970.

So what? you say, integers are all represented in 32-bit registers these days, aren’t they? That’s more than enough space to represent numbers bigger than 230.

First of all, note that we’re using signed integers, which means that one of those 32 bits is being used to tell us whether or not the number is positive or negative. Then, for more deep and dark reasons, our ML implementation uses another bit of those 32 to “tag” its integers (to distinguish them from other possibilities). This means that our ML has a maximum integer value of 230 − 1, and this was exceeded on 10 January.

And lo, we were much surprised. Code that was working fine before the weekend stopped working on the Monday. Our beautiful programs, pristine in their Platonic perfection, were actually dependent on the environment, the tick-tick-tick of passing time, and this dependency twirled ’round and bit back.

Luckily, we can also convert times into floating point numbers that use more than 32 bits, so we’re safe for the moment. Nonetheless all our users are going to have to upgrade their system. (Roll on the day when our ML has an arbitrary precision integer type built in.)

Wednesday, 17 December 2003

Feeble excuses

Listening to:

Bach, English Suite no. 5, BWV 810.

Still reading:

Popper, The open society and its enemies. I finished the first volume (The spell of Plato) a little while ago, and am now up to Marx and Hegel. On a recent weekend away to Melbourne, I started Patrick O’Brian’s The thirteen-gun salute (more plane reading), but didn’t finish it. This puts me in the awful position of having two books to read at once!

My long absence from this page is not just a matter of slackness. Oh no. The first two weeks of December were given over to the Logic and Automated Reasoning Summer School. I found this pretty full-on, and I only went to two out of five lectures a day, and some of the seminars. Students, who were encouraged to attend everything, and probably all had less of a background in logic than I had, no doubt found it all quite overwhelming. (I’m sure I would have.) In some lectures, I already knew some of the material in a bitty way, as if I’d picked it up by osmosis, say. I went to these lectures because I wanted to see the material presented more formally, so that I subsequently might be able to honestly claim that I really did know something about it. (It was interesting too, of course!)

I also gave a lecture and a seminar myself. In both cases, I went in somewhat worried that I didn’t have enough to say, but found myself with not enough time. Five already sketchy slides on Cooper’s algorithm (from the end of this presentation), presented at haste, assuredly did no-one any good whatsoever. I think the description of Fourier-Motzkin and the Omega Test went across well though.

I leave you with this interesting and amusing analysis of procrastination.

Monday, 1 December 2003

Mahler, Milner and gross consumerism

Listening to:

Mahler, Das Lied von der Erde. Cod-Chinese poetry from the late 19th century

Look down there! In the moonlight on the graves
there crouches a wild and ghostly form—
it is an ape! Listen, how its howling
rings out amidst the sweet scent of life!

set to stunning music.

  • Consumerism leads to excess in the USA.

  • An interesting interview with Robin Milner, the fourth most cited author in Computer Science, and generally impressive guy. Before the interview moves onto more technical material, there’s much of general interest in Milner’s early career and schooling. For example, he’s amusing on having to do Latin and Greek at Eton.

    I was pleased with myself for spotting the way in which the interviewer and Milner use slightly different idioms of English. For example, the interviewer mentions Milner going to Edinburgh to take up a professorship. Milner corrects this to “lectureship”. The interviewer also talks about “math”, while Milner says “maths”.

Friday, 21 November 2003

Voting computers

Listening to:

Mozart, symphony no. 27 in G major, K. 199.

A work-related link: a story from Wired about voting computers. There’s a right way to do things (that’s the Australian way, and given the stamp of approval by ANU academics), and a wrong way (as done in the US). (If you want more than my gross simplification, read the article.) And there’s more: in recent top secret developments, I have become involved in work looking at applying the mighty power of Formal Methods to make that stamp of approval even more impressive.

PS: Australian copyright law really sucks, and music industry types think so too.

Friday, 7 November 2003

Phew!

Listening to:

Ella Fitzgerald singing the Cole Porter song book.

I’ve just spent much of today writing some course material to accompany the one(!) lecture I’m giving as part of the department’s Logic Summer School. You can even get it from my new home-page. (This has been carefully set up with redirects and the like to mask my old Cambridge existence—très Orwellian).

Tuesday, 5 August 2003

Category theory

Listening to:

Sullivan, cello concerto.

Now reading:

Charles Dickens, Little Dorrit.

Faster wireless networking.

I didn’t write yesterday because I had to spend a chunk of my day getting my head of little brain around the excessively abstract stuff called Category Theory. (This is another of those maths fields where it’s far from clear why the name x of x Theory has been chosen. What, for another example, is so groupish about the objects of study in Group Theory?)

There’s quite a comprehensive looking introduction in the Wikipedia, which includes the line

Category theory is half-jokingly known as “abstract nonsense”.

Finally, a quote that I found and liked recently:

For books are not absolutely dead things, but do contain a potency of life in them to be as active as that soul was whose progeny they are; nay, they do preserve as in a vial the purest efficacy and extraction of that living intellect that bred them.

I’ll reveal the source next time (ooh, the excitement).

Thursday, 31 July 2003

Latest Mozilla & a power cut

Listening to:

Haydn, string quartet no. 63 in B flat major, Hob. III:78 (Op. 76 No. 4) ‘Sunrise’.

A cool optical illusion.

I recently upgraded my version of the Mozilla Phoenix/Firebird browser from 0.4 to 0.6. I had thought this was going to be a major undertaking, and that I would find it difficult because I don’t have the root password on my lap-top, and I didn’t really want to be installing software as root if I could avoid it anyway.

But it all worked fine: I could install it as an ordinary user without any problem, and my bookmarks also transferred. I even successfully downloaded a Java plug-in. I haven't tried to get Flash working yet. The new version fixes some bugs, and has some very nice features. Tabbed browsing is particularly good. This allows you to open multiple web-pages within one window. You can switch between them by clicking on “tabs” that poke up above the currently displayed page like the way folders in a filing cabinet work. I can open up a folder of bookmarks (my “morning run”) in a string of tabs, and they all load in parallel. By the time I've finished looking at the first couple of pages, everything else is all loaded up, and switching from one to the next is as simple as hitting Control-W to close the current tab and move on to the next.

While writing this, the building suffered a power cut. The lights went out, a loud cry of Shit!! was heard from my neighbour, but my lap-top just kept on going. It will be interesting to see if its battery expires before the power comes back on. Because I’m running it a bit hard at the moment with some work (I think my latest change to HOL is an improvement functionality-wise, but I think it may have also made some things a bit slower), the fan is coming on pretty frequently. Apart from this, there’s no other noise. Quiet can be so delicious.

But that quiet means there's no air-flow in the building, and we've just been told over the building PA's system that an early lunch might be advisable as a result. My battery power meter says 28 minutes remaining, but even if it lasts a while longer, I won't be able to upload this until main power is restored because at least some of the network switches between here and Jamie’s cupboard are not working.

Friday, 25 July 2003

Storage issues (+ sex and media tittle tattle)

Listening to:

Dvořák, The water goblin.

The Guardian newspaper is moving to the US. So says this article from New York magazine. There’s nothing wrong with a bit of optimism on the part of The Guardian’s owners I guess, but it does seem pretty unlikely to succeed.

Now that prostitution has been legalised in New Zealand, an Auckland brothel called Monica’s has been advertising for staff. This has annoyed the US Embassy in NZ, because the advert used an American style crest with crossed American flags and a bald eagle logo, and the ‘club’ is described as being downstairs at The White House. (The BBC.) It all smacks of a conspiracy to wind up Americans.

To close on a more serious note, this is an interesting article about the state of computer storage today. Disks are getting bigger at an incredible rate: densities are doubling every year, and I guess that means capacities are not far behind. But the speed at which data can be retrieved from disks has only been improving at a rate of 7 to 10 percent each year. Networks certainly can’t keep up with this increase in storage capacity either, so one of the people interviewed in this article talks about how he finds it easiest to just mail whole computers to his colleagues rather than attempting to transfer the data over the Internet.

Wednesday, 9 July 2003

Proofs and computers

Listening to:

Francesco Silvestrino, O dio se vede chiaro. From a BBC Music Magazine CD called The Glory of Venice, featuring 16th century Venetian music.

Weapons of mass destruction; can’t live with ’em, can’t live without ’em.

A recent article from Nature on a proof whose status is unclear because a computer was used to check lots of tedious cases. The proof of the four colour theorem was also constructed with a computer's help and is viewed with similar suspicion. (But maybe a proof in a theorem-proving system would be worthy of more respect? Some people are working on this, including Gertrud Bauer and Tobias Nipkow.)

A nice article on irony, what it is and isn’t.

Thursday, 5 June 2003

Hot Gingerbread and Dynamite

Listening to:

Schubert, string quintet in C, D 956. I seem to be timing my entries to coincide with Schubert listening quite a bit these days.

Formal Methods—useful?

I was away in Sydney at the end of last week for a NICTA workshop on Formal Methods. The venue was the Scientia building on the UNSW campus. I had a pleasant three days, gave a talk that prompted some interested sounding questions, and heard lots of interesting talks by others.

As is often the case at these sorts of gatherings, there was a bit of soul-searching about the utility of what we’re doing. Carroll Morgan put it nicely when he said that we shouldn’t be too harsh on ourselves, and that FM suffers a little from the same problems as AI, the perception that

If it’s not boring, it can’t be Formal Methods.

The problem is that academic theory takes a long time to filter out into industrial practice (and not all theory is going to make it either, of course; some of it’s no use to man nor beast). Someone working on theory now may well have to wait an awfully long time in order to see their work gain a broader acceptance. And given the failure rate, how can they be sure of its real worth?

Finally, my last word on The matrix:

  • The Republican Matrix.

  • This article analyses the film from a religious and/or philosophical point of view, and finds all sorts of interesting stuff in it. This is all very well though I can’t help suspect that you’d find all sorts of interesting stuff in just about anything if you looked hard enough, and if you knew what you were going to find in advance. My problem with The matrix is more that it’s poor science-fiction, and any amount of religious imagery doesn’t alter that.

  • On the other hand, it is an entertaining film.

Wednesday, 14 May 2003

Irritated by Paul Graham (w/fruit juice on the side)

Listening to:

Schubert, Overture “in the Italian style”, D590.

My toe is rather an ugly purple colour on top, but my gait is less of a hobble than it was on Monday, so I think things are on the mend.

Here's a marker of cultural difference between the UK and Australia (other than: one can play cricket, and the other can't): in the UK you can buy orange and grapefruit juice blends in cartons. This is typically known as ‘breakfast juice’. In Australia, you can't (I have seen ‘breakfast juices’, but these are typically orange with mango and/or pineapple). But Australia distinguishes itself by providing apple and blackcurrant juice, which I don't remember seeing on the shelves at Sainsbury's. Australia's better because you can mimic the UK by buying the orange and grapefruit juices separately, and mixing them yourself, but you can't buy blackcurrant juice separately in either country. Isn't that fascinating?

There's a guy out there called Paul Graham who is definitely something of a guru. I earlier linked to a piece of his about using Bayesian analyses to detect spams (given samples of non-spam and spam messages). For whatever reason, his proposal hit a nerve, and lots of people rushed to implement this (good) idea. I am using Xavier Leroy's SpamOracle implementation of this idea, and it works wonderfully.

On the other hand, Graham's latest piece is all about hacking and how it's really just like painting, and it gets up my nose in all sorts of ways. Perhaps this is inevitable. He says

I've never liked the term "computer science." The main reason I don't like it is that there's no such thing. Computer science is a grab bag of tenuously related areas thrown together by an accident of history, like Yugoslavia.

and I just don't buy this. Yes, there's a spectrum of interests in a Computer Science department, but this is true of any discipline too. Graham's also got a real hang-up about what he calls static typing, and he proffers Lisp's dynamic typing as a real win over languages where you have to declare the type of every variable (from another essay of his). SML and Haskell are both statically typed languages, and neither requires you to declare the types of variables.

Of course, both of these languages are academic languages (i.e., the product of academic research), and academia is generally getting a bum rap here so perhaps it's not surprising that I should feel so antsy. It's all symptomatic of a typical mentality that says that hacking is cool, and where the real work is done, while stuff done in ivory towers is obviously not useful, or applicable to the practice of real programming. In order to demonstrate that they absolutely don't suffer from maths envy, people of this view find it too easy to lurch to the opposite extreme and dismiss academic stuff out of hand.

Seethe, seethe.

Thursday, 10 April 2003

XHTML & code maintenance

Listening to:

Shostakovich, piano sonata #2, op 61.

I couldn’t resist the temptation; I’ve made my page XHTML. Again, work done just so that the page looks exactly the same as it used to. But it’s better, honest! It’s fully standards compliant, and easily upgradable, and flexible and it might even be easily viewable on mobile phones! (Oh yes, I know that I have legions of devoted fans reading this on their phones.)

It’s funny the way maintaining code works. If there’s enough of it, you can be sure that there will be all sorts of bugs in it, or that bugs will appear in response to various incremental changes. Fixing a slew of problems in HOL recently, I decided that what I was doing was analogous to carefully examining a patch of soil in a garden, walking slowly in a stooped posture, and looking for weeds or noxious insects. You’re forced to turn over every stone, and scrutinise everything at length. Of course, if we had extensive regression test suites, some of this work could be done automatically...

Some links:

Wednesday, 23 October 2002

Snipers; MS & open source; Mozilla

Listening to:

Verdi, Otello.

Matthew Engel on normal life in places that become the centre of media attention, with particular reference to Montgomery County, Maryland (sniper country).

An article from C|Net news.com about Microsoft and its changing attitude towards open source.

A pretty positive review of Mozilla. (I don't know why we were given Netscape 6, when we could have Mozilla or Netscape 7 instead.) A fairly speculative article from Salon about the import of Mozilla and how it may be a significant platform for further software development.

Friday, 18 October 2002

Unicode will eat your brain

Listening to:

Vaughan-Williams, symphony no. 8 in D minor.

Once upon a time, deciding that this log shouldn't just be me wittering on about trivialities, interspersed with book reviews, I tried to start a discussion of something fairly technical and work related. (Others do this quite successfully. I've recently become a reader of Raph Levien's online diary, where Raph talks all about proof systems and other stuff near and dear to my heart.) Sadly, I never got beyond Part II of my discussion on higher order matching. But why? Well, now the truth can be told.

It's all the fault of standards zealots in the land of fonts. In order to discuss higher order matching, I needed to be able to write the Greek symbol lambda, and I couldn't get this working under Netscape 4 (and it doesn't work under Netscape 6 either). Yes, my maths would look OK under Internet Explorer, but I didn't (and don't) have such easy access to that browser. For all that 90% of my readers would see my lambda's OK, I wanted to see them too. But it seems that the device whereby the mathematical symbols are made available for Explorer is not standard, and Netscape doesn't support it. We should be using Unicode instead apparently. (A comprehensible explanation of the problem, a cute illustrative page.)

It seems to me that people who get involved in the worlds of computer fonts quickly lose all of their previous usefulness in other fields. Computer fonts suck them in, chew them up and they're never the same again. My attitude is one of wilful ignorance; I just don't want to have to know about three levels of abstraction, and vocabulary like glyph and charset.

Friday, 20 September 2002

Why I do what I do

Listening to:

Mozart, string quartet no. 15 in D minor, K421.

I’m still writing slides, and this will be an all-consuming activity.

In the meantime, you might like to read this neat manifesto, explaining why someone might like to mechanise mathematics. I think the computer science applications that Freek downplays are interesting too, but it’s certainly true that they are very tedious. (The art is in making them less so.)

Friday, 9 August 2002

Computer science and intellectual property

Listening to:

Beethoven, sonata no. 1 in F, op. 5 no. 1 for piano and cello.

The famous computer scientist, Edsger Dijkstra, died on Tuesday. His work, a significant part of what passed to me through the people that taught me as an under-graduate, inspired my decision to come to Cambridge to do my PhD.

Ross Anderson reckons that the University of Cambridge is about to shoot itself in the foot, by demanding rights to its academics’ intellectual property. Up ’til now, the university has spawned useful links with companies within the region. I can offer some personal evidence: our departmental pigeon-holes have just been rearranged so that the pigeon-holes companies working within the lab are all grouped together. There’s quite an impressive column of them all. Though not all of them will necessarily make it, there’s a good chance that a high proportion will make their way into the wider world and become successful companies, generating money and jobs. Nonetheless, the University claims that this success is nothing to do with its current liberal intellectual property rules.

Worse still, the proposal might prevent academics from giving their property away for free. I’m not directly a university employee (being employed by a university college, St. Catharine’s, instead), but I’d be pretty hacked off if some university bureaucrat told me that I couldn’t make my work on HOL freely available.

This piece from the Observer (also linked to from Ross’s site), is one of a number of polemical responses. I was amused to think of myself as a “hot-house plant”, only able to blossom under certain conditions.

Friday, 26 July 2002

Bumps, Japanese radishes and Cthulhu

Listening to:

Mozart, Spaur-Messe, K258.

We were bumped yesterday, so we’re now down 3. The appealed bump from Wednesday night even made the last three paragraphs in the local newspaper's reporting of the bumps. If we get bumped again today, then we have won our ‘spoons’ (contrast with the ‘blades’ that you win if you go up four places).

Other stuff:

  • A Cthulhu/chess story
  • I went to a very interesting talk yesterday about the Daikon system for automatically guessing program invariants.

Thursday, 28 February 2002

JavaScript

Listening to:

Shostakovich, string quartet no. 3 in F major, op. 73.

In my travels around the web, I usually keep JavaScript turned off. With it on, I usually get more grief than help. The browser seems more liable to crash for a start, but I also get all sorts of garbage dumped on me by web-page authors who think that their scripting skills make all the difference to their page. Given that most of the effects are pure glitz, I just find this attitude annoying. Sometimes JavaScript is even worse; it pops up extra windows, ignores my font size specifications and is generally a nuisance. For example, the Hunger Site now uses JavaScript to do that annoying window pop-up thing.

On the other hand, the JavaScript effect on this page deserves to be seen. Yes, it’s annoying and impractical, but it’s cool. (Waggle your mouse around a bit.)

Elsewhere:

Tuesday, 23 October 2001

Calculating π and the war on terror

Listening to:

Shostakovich, symphony no. 8 in C minor, op. 65.

Still reading:

James Joyce, Ulysses. I read three sections over the weekend: Aeolus (in a newspaper office), The Lestrygonians (Bloom looks for lunch), and Scylla and Charybdis (Stephen Dedalus argues about Hamlet and Shakespeare’s life in the library). I’ve now read nine of the eighteen sections.

Did you know that you can get good estimates for the value of PI by just looking at your own files? It’s all down to number theory and the ratio of relatively prime pairs of numbers to non-prime pairs. (A number x is relatively prime with respect to y if x and y have no common factors. For example, 10 and 21 are relatively prime, even though neither of them is prime.) See this neat page for more details, and Real Code. (The same guy’s site includes a very good description of his PhD research; I’d like to write something similar about mine.)

Some “war on terrorism” links:

  • The Onion is generally a pretty good source of satire. This issue is from 26 September, and is very good, including headlines like US vows to defeat whoever it is we’re at war with and God angrily clarifies “Don’t kill” rule. More recently, this piece makes the civil liberties argument very well (though perhaps laying it on a bit thick).
  • The Boston Globe finds evidence that private security firms, the airlines and the FAA were all getting a bit cosy about security responsibilities at Logan Airport before 11 September. For example, on the possible forms of security tests:

    “We didn’t want everyone testing us without knowing what to look for exactly,” Bibbey, the Logan manager for Globe Aviation Services, said in an interview. “We don’t need people improvising test pieces to purposely make people fail.”

  • The LA Times on the Arab TV channel Al Jazeera, and how it is providing a valuable service.
  • Finally, a discussion from the Washington Post about civilian casualties as a result of bombing Afghanistan.

Thursday, 18 October 2001

Omega Test busy-ness.

Listening to:

Bach, Art of the fugue.

Still reading:

James Joyce, Ulysses. Read “The lotus-eaters” and “Hades” over the weekend.

Very brief entry today because I’m far too busy making sense of the Omega Test.

Thursday, 4 October 2001

Software runaways and more

Listening to:

Puccini, La Bohème.

Holiday reading:

Robert L. Glass, Software runaways.

I read this in Australia because it was in a friend’s book-case, not because I took it with me. It’s a repackaged collection of articles, including a big chunk of someone else’s masters thesis, about software projects that went disastrously wrong, usually costing the earth, and/or taking much longer than expected to finish, or not finishing at all.

As a collection, it doesn’t hold together particularly well. The introduction is OK in terms of introducing Glass’s theories about project failure, but the rest of the book makes pretty dull reading. Many of the failures were due to political squabbles (rather than bad technical decisions), but there’s nothing much in the way of human interest in the presentation of these stories. Further, the technical problems are not described in anything like enough detail to allow anyone to take away any sort of technical lessons.

My link du jour is (part of) the sad story of how more and more free “content” on the web is disappearing. The New York Times hasn’t given free access to its standard archive for a while, but as a result of the Tasini case explained above, it has now removed lots of pre-1995 book reviews from its site that were apparently available before. The New York Review of Books is doing something similar, and Salon has moved most of its politics coverage to subscriber-only access.

However, Salon does have this neat article/review of Ursula K. Le Guin’s latest Earthsea books available for all. (OK, I admit it, I call it “neat” because I find myself in almost complete agreement with the reviewer about everything she says.) I just hope it continues to remain accessible indefinitely.

Friday, 3 August 2001

Shrek and the forgotten web

Listening to:

Bach, The well-tempered clavier, book 2.

A recent movie:

Shrek. A computer-animated movie, nominally targetting children, but really quite amusing and entertaining for adults as well. Toy Story 2 is also very good in this respect. Shrek wins by not having a nauseating song in the middle about growing up; Toy Story 2 has a better ensemble cast.

Old forms of the web

I came to what I thought was an interesting realisation the other day: the Web is almost of necessity backwards compatible. By this I mean that producers of pages can be sure of getting their message across by sticking to basic HTML because browsers can’t afford to throw away that functionality. As an extreme example of this, just look at the way you can still access GopherSpace. Follow this link (possible in Netscape, Internet Explorer and Lynx, at the very least) and you’re no longer in the world of HTML. You’re navigating through a strange, isolated world with lots of dead links, but still the browsers let you do it.

Introducing backwards incompatibilities in a program that you want other people to use is a generally a bad thing. With something like a compiler or a word processor, the incompatibilities can mean that the user has to alter their files. This can be enough of a pain to give the developer pause. But if their new browser is backwards incompatible in such a way that it fails to display pages that it used to display, and these pages are (naturally) beyond the power of the user to change, then that browser is hardly going to win itself many converts.

While support for the gopher protocol may disappear because fewer and fewer people are using Gopher servers, HTML seems to have become seriously entrenched. (So much so that I remember reading an interesting article a while back about the fact that so much of the information in URLs is coming to be seen as redundant; how many company advertisements bother with http://www.company.com? Most just go for company.com; everyone knows to add the other stuff, or their browser does it for them.) This entrenchment means there is a great inertia protecting all those plain HTML pages. ASCII is assuredly safer, but HTML is getting there too.

Thursday, 19 July 2001

Just one more X

Listening to:

Brahms, clarinet trio in A minor, op. 114.

There’s a certain class of computer games out there, sometimes characterised as 4X games (“eXplore”, “eXpand”, “eXploit” and “eXterminate” or some such), that are known for their addictive “just one more turn” qualities. The first game in this mold was probably Civilisation, where the player has to control a civilisation from its earliest beginnings all the way to the point where it is ready to send a space-ship to Alpha Centauri. (This PC game has only a very tenuous connection to the classic board-game of the same name.)

I’d just like to briefly claim that interactive theorem-proving is subject to a similar phenomenon, which I (and others) call “just one more lemma”. Say you’re trying to prove big complicated theorem X. You spend a while on this before realising that you can’t prove it, without first proving supporting lemma Y. But then it becomes clear that Y needs a theorem about lists that the developers of the system haven’t included (incredulously you think to yourself, “How on earth could anyone ever prove anything without first knowing that MEM x (FILTER P l) = MEM x l /\ P x ? I mean; come on!”)

These “to prove X, I will first need Y” links build into ever larger stacks. In fact, it can become easy to lose track of the original goal entirely. But now, I have to go and prove sub-lemma Z103.

Thursday, 5 July 2001

Entry #192

Listening to:
Bax, symphony no. 3.
Higher order matching, part II. (Part I.) Before even discussing the algorithm, we have to decide on what it means to do matching of function symbols. Consider the pattern X(a,b) and the term f(b,a). If all we allowed was the possibility of instantiating X with f (or some other symbol), then there wouldn't be a match here. But this is dull. In fact, it's really just first order matching all over again. We could translate every term of the form f(x1,...xn) (where any of the f and the xi arguments might be variables that could be instantiated) into app(f,x1,...xn). The app would be a ``constant''; i.e., not instantiable, and the problem would be entirely first-order.

Consider again our pattern X(a,b), and the term f(b,a). Really, we'd like to be able to instantiate X to the function that takes a pair of arguments, flips them, and then passes the result onto f. In other words, let's imagine that there's a function out there called g, and that g(x,y) = f(y,x), for all possible arguments x and y. Then, instantiating X with g would do the trick.

Notice how I did two things in the previous paragraph. First, I came up with a description of what I wanted my function to do, and then I invented a name for it (g). Now, this second step is un-necessary if we use lambda calculus notation for writing down functions. So, next time, I will talk about just that.

Wednesday, 27 June 2001

Higher Order Matching I

Listening to:

Mozart, piano quartet in G minor, K478. (The CD traversal continues.)

I want to explain higher order matching. But before I can even get onto this, I should first discuss first order matching. Here goes: if I have the term f(X,a), is there any way of instantiating the variable X so as to make the term the same as f(b,a)? Obviously there is; just set X to be b. Similarly, it should be easy to see that there is a match between the pattern term f(X,g(Y)) (where the variables we are allowed to instantiate are X and Y; the convention is that the upper-case letters are variables that can be matched, and that the lower-case letters can’t be instantiated) and the term f(h(a),g(c)). Equally, there is clearly no way to match the pattern f(X) to g(a). There are more interesting ways to fail too. Consider trying to match the pattern f(X,g(X)) against f(a,g(b)). This can’t succeed because we would have to simultaneously instantiate X to a and b.

There’s a pretty easy algorithm for determining whether or not a match exists between a pattern and a term. Basically, the two terms need to be traversed in parallel with an environment being maintained along-side to record what instantiations you’ve made so far. When you come to a variable in the pattern term, you first check to see if that variable has already been instantiated. If so, check if its instantiation is the same as the thing you’re matching against; if not, fail. If the variable hasn’t been instantiated so far, record it as being instantiated with the concrete term you're matching against.

The thing that makes this first order matching is the fact that variables in the pattern term mustn’t take arguments. In other words, f(X(a),Y) is an illegal pattern because of the use of X as a function (taking argument a). Next time I will explain how the shift to the higher order problem is done.

Wednesday, 2 May 2001

Bread and roses; computer science

Listening to:

Fauré, piano quartet no. 1 in C minor, op. 15.

A recent movie:

Bread and roses. This film is directed by Ken Loach, quite a famous British director. I’d never seen anything by him before seeing this film though. I read a review of the film before going to see it that suggested it was a bit of a polemic, and this verdict is accurate I think. The story is all about a young Mexican woman who illegally crosses the border into California, and gets a job as a janitor. Her job is with a exploitative non-union company, and the crux of the movie is her (and her workmates’) struggle for better conditions.

The acting, particularly of the three main characters: the woman, her older sister, and the union rep, is good and the plot has some good twists and turns. However, the film is also blatant, one-sided propaganda. It’s not the content of the propaganda I have a problem with, but the simple fact that it is propaganda. None of the obvious arguments against the film’s thesis are even mentioned, let alone replied to. If you can get over the irritation of being preached to, then you may well find this film quite enjoyable.

The predicted May-day riots in London didn't really eventuate yesterday. The police were better organised than the anarchists (but then, you might expect that; anarchists representing the antithesis of organisation, right?), and contained the various potential problems. So much so in fact, that you couldn’t help but think that the non-violent protesters got a raw deal. Perhaps they should have asked the police permission for a march. Getting official permission might not be that easy, and doing deals with the state might be anathema for your typical anarchist. Try this page for a (brief) humorous slant on it all.

A little “maths” problem that was discussed at tea recently:

Is it always possible to write a bitstring of length 2 to the n, such that all the possible bitstrings of length n are present (including wrap-around)?

For example, 0011 is the only possible solution (modulo rotations) for n = 2. The string 10 is present because of the wrap-around, and the other three possibilities are all obviously there. A solution for n = 3 is 00010111.

Finally, a little something from Usenet:

Good code in perl is fine, but there's something about bad code in perl thats worse than bad code in other languages, something very HP- Lovecraft-mad-servants-of-the-elder-gods-chattering-in-the-extra- dimensional-insect-language kind of bad that makes my head hurt when I have to read it. ["Jish Karoshi" <karoshijish@hotmail.com> in c.l.ruby]

Friday, 6 April 2001

HOL training

Listening to:

Mendelssohn, symphony no. 3 in A minor, op. 56 “Scottish”. Felix did actually go to Scotland at one point, so it seems reasonable that he should have been inspired by what he found there. I’m currently up to the sprightly second movement (Vivace non troppo), which opens with a gorgeous theme on the woodwind.

Foo and more

A reader suggests this variation on the bee poem:

I'm as busy as a bee with a bum full of honey

but we agreed that mine is better.

Ever wondered about this foo word that computer-geeks seems so fond of? Now, there’s an RFC explaining all. It's an April Fools RFC, but this doesn’t make it any less informative.

The work that has been keeping me so busy recently (running 'round like a blue-arsed fly even) involved the production of many, many slides to be used as training materials for the teaching of the HOL system. I’m just about done now, and happy to say that if you want to see my handiwork, you can do so here. The slides were all produced with the Prosper style for LaTeX.

Another part of the project involved the creation of a "case-study" proving confluence for combinatory logic. Combinatory logic is what underlies the neat obfuscated programming language Unlambda (it even has a Comprehensive Archive Network, like TeX, and Perl).

Thursday, 29 March 2001

Bloatware

Listening to:

Beethoven, sonata no. 3 in A, op 69 for piano and cello.

A recent movie:

Toy Story II. I saw this at home on DVD recently, and thought it was brilliant. It has a rather gag-inducing song in the middle about a girl growing up and abandoning her toys, but it's otherwise extremely amusing and entertaining. On DVD, we also got to see a bunch of interviews with some of the actors doing the voices, which was kinda neat.

Joel gets it wrong

I’m going to link to Joel Spolsky again today, but this time I come not to praise him, but to bury him. His latest article is about bloat-ware. This is the phenomenon that sees the 1993 installation of Microsoft Excel take up 15 MB of disk-space, and the version for 2000 take up 146 MB. He dismisses complaints about this problem by saying that the decreasing cost of hard-disk space has more than made up for the increase in size, so that in terms of its space-consumption cost, the 2000 version of Excel is actually cheaper than its predecessor. He also dismisses complaints about the fact that big programs have a memory-consumption cost too (some part of them needs to be loaded into memory); pointing out that paging and virtual memory combine to ensure that you may not often have much of the executable in memory at any one time, and the rest will be consuming more of that cheap disk-space. Further, this means that start-up times for the application will likely be pretty good.

So far, so good. This stuff is all perfectly correct. But it’s not the real reason to feel annoyed about bloatware. My objection to it is that it’s a sign of poor craftsmanship. Does Spolsky really think that it's admirable that at least some versions of Excel include a flight simulator Easter Egg?

He explains bloatware thus:

In fact there are lots of great reasons for bloatware. For one, if programmers don’t have to worry about how large their code is, they can ship it sooner. And that means you get more features, and features make your life better (when you use them) and don’t usually hurt (when you don’t). If your software vendor stops, before shipping, and spends two months squeezing the code down to make it 50% smaller, the net benefit to you is going to be imperceptible. Maybe, just maybe, if you tend to keep your hard drive full, that's one more Duran Duran MP3 you can download.

That looks like one dodgy reason to me, not lots of great ones. If shipping software quickly is the overriding concern, then the result may well be better results for the company producing the code, but what does the consumer get? Insufficiently debugged, poorly tested code that crashes more than it should. Maybe all of those features that have been pushed into the new program are interacting in subtle ways with the flight simulator. Maybe the fact that several versions of the same library code have been linked with the application is an indication that the people developing the code didn't really have any idea about what they were doing when they wrote it.

Would you buy an operating system from these people?

Wednesday, 7 March 2001

Entry #150

Listening to:

Bartok, string quartet no. 4, (Sz 91)

LaTeX Slides

I’m working on some slides, and I just have to plug a neat package called Prosper. It lets me use LaTeX to write my slides (complete with all of LaTeX’s great mathematics type-setting), and produces results that look suitably PowerPoint-ish. An alternative technology is TeXPoint, which allows the embedding of TeX/LaTeX material directly into PowerPoint slides. I might use this if it weren’t for the fact that I’m redoing a whole bunch of slides that were originally pure LaTeX.

Thursday, 1 February 2001

Death of Pascal

Listening to:

Mozart, string trio (divertimento) in E flat, KV 563. And there I was claiming that Mozart’s letter was K. I think the V here is the same as the V in Bach’s BWV, and that it means something like catalogue. The music is great in any case.

Perl Scripts and Pascal

I have re-organised my archived weblog entries so that reading down the page does move the reader forward in time. I have also added next month and last month buttons to them all, just as I have done here. To achieve the reordering I used the following Perl script:

$/ = "<hr>\n";

while (<>) { $foo[$i++] = $_; }
while ($i > 0) { print $foo[--$i]; }

(Historical accuracy forces me to admit to the above, but it would have been even more idiomatic if I’d used Perl’s push and pop functions.) My code assumes that the entries are delimited by <hr> (horizontal rule) elements. There’s also a whole bunch of stuff in front of the listing of the entries (the table setup, etc), and some after it. But this didn’t really matter because I used the facility in Emacs whereby you can select a region of text, pipe it to some external program, and have the program’s output replace what you had there originally. (Lest I be accused of editor-zealotry, let me add that you can do the same thing in vi.)

Before I leave you for the week, let me first say a few words about this article, another one from Salon about programming languages. This one is about the language Pascal, and how it’s gradually dying out. I don’t have too much problem with this report; it seems that Pascal really only holds out in the Delphi product. However, I really barfed at the following paragraph:

Pascal took a very mathematical approach to creating software: It forced the programmer to specify the type of each piece of data. That is, the programmer had to spell out whether variable x held some text, an integer or a real number. This didn’t prevent the programmer from doing something stupid like dividing by zero, but it allowed the compiler to stop the computer from doing something really stupid – like trying to multiply the word “rabbits” by 23. After Pascal’s birth in the early ’70s, the mathematicians in university computer sciences grooved on the complicated hierarchies created by type-checking a program.

As any reasonably qualified computer scientist could tell you, Pascal’s type system is not very mathematical at all. It certainly doesn’t feature any of the complicated hierarchies that get the type theorists going. It’s certainly a deal less sophisticated than the system in C++. But, if you want real sophistication, you use a language like SML, where you don’t need to specify the types of many variables at all, because it figures them out for you, using what’s known as type inference, but where you still get such groovy features as parametric polymorphic and higher order functions. (Check out this outline of a nice talk, for an explanation of what strong typing really is, intended for an audience of Perl people.)

And now for another bogosity:

Meanwhile, Pascal’s development splintered as people argued over the right way to do things. It’s almost as if the Pascal community acted like the French by defending the purity of their language – while the C++ world acted like the English, promiscuously absorbing words from other languages.

If Pascal was splintering, it can hardly be said to have been doing a great job of defending its purity. If it was splintering, it was in fact doing a reasonable job of trying to find itself a niche, with little regard for purity. Maybe Delphi is its only viable niche, right now, but hey, it’s a perfectly reasonable niche. The argument’s crap but just look at the way this author is setting up a really dirty set of connotations with which to tar Pascal. In the first paragraph, it’s academic and mathematical. (Real programmers don’t do maths, sheesh!) In the second, we cunningly associate Pascal with France, that well-known bastion of anti-capitalist un-American head-in-the-sand isolationism.

Disclaimer: Pascal was my first real programming language, but I haven't written in Pascal since 1990, and have no desire to ever do so again.

Friday, 9 June 2000

Mahler, and writing

Listening to:

Mahler, symphony #3. This is Mahler’s longest symphony, and the longest symphony of anyone’s commonly performed. My recording (on Naxos), takes one hour and forty-one minutes. Of it, Mahler said that it should contain all nature.

Writing

My entry deficit is finally beaten with this entry. I am back to my three-a-week average, and is all well with the world.

I’m currently writing an article which really needs to be submitted today, so I will be terse, and say just to look out for it in the Computer Journal.

“That’s hubris, that is.”
“Yeah, I’ll say; cocky authors, who d’they think they are?”

Friday, 14 April 2000

Work and play

Listening to:

Pink Floyd Dark side of the moon. My office-mate is having a week and a half off in the US. My neighbour is also away all this week. This means that I can dispense with the headphones, and listen to my music the way nature intended! :-)

Work-list, play list

Work, work, work. Cooper's algorithm for deciding Presburger arithmetic, the semantics of C, contexts, action calculi, the lambda calculus, type systems, subject reduction, interactive theorem proving.

Play, play, a little. If music be the food of love, play on, swimming, badminton, games on computers or not, big college feasts in honour of ancient benefactors.

And there I must leave you, because both of the above are today taking precedence over my compulsion to document my life.

Thursday, 3 February 2000

Moscow ML

So, I'm a computer science researcher, and it's time to add a plug for the great Moscow ML implementation. I use this underneath the hol98 theorem proving system to do my stuff.

I’m feeling particularly lyrical about this system today because the principal implementor, Peter Sestoft has found and fixed a problem I was having in under a week.