peteg's blog

More introspection from the Czech master, a dry run for his four-years-in-the-future Unbearable Lightness of Being. I have to say that Teresa and Sabina resolve into foxier women in the latter than poor Tamina does here.

This is fairly standard territory for him, combining sex, politics, literature and authorial interjection in a ramble about the necessity of memory and the power of laughter. He gets the big quote from the book out of the way on the first page:

It is 1971, and Mirek says that the struggle of man against power is the struggle of memory against forgetting.

Kundera is never short of an idea or shy in defending one. What sticks in my memory is his characterisation of "the two types of laughter" in The Angels (the first one, p61 in my English translation):

...

Angels are partisan not of Good, but of divine creation. The Devil, on the other hand, denies all rational meaning to God's world.

...

Things derived suddenly of their putative meaning, the place assigned to them in the ostensible order of things ... make us laugh. Initially, therefore, laughter is the province of the Devil. It has a certain malice to it (things have turned out differently from the way they tried to seem), but a certain beneficient relief as well (things are looser than they seemed, we have greater latitude in living with them, their gravity does not oppress us).

The first time an angel heard the Devil's laughter, he was horrified. ... [U]nable to fabricate anything of his own, he simply turned his enemy's tactics against him. He opened his mouth and let out a wobbly, breathy sound in the upper reaches of his vocal register ... and endowed it with the opposite meaning. Whereas the Devil's laughter pointed up the meaninglessness of things, the angel's shout rejoiced in how rationally organised, well conceived, beautiful, good, and sensible everything was on Earth.

... And seeing the laughing angel, the Devil laughed all the harder, all the louder, all the more openly, because the laughing angel was infinitely laughable.

Laughable laughter is cataclysmic. And even so, the angels have gained something by it. They have tricked us all with their semantic hoax. Their imitation laughter and its original (the Devil's) have the same name. People nowadays do not even realise that one and the same external phenomenon embraces two ompletely contradictory internal attitudes. There are two kinds of laughter, and we lack the words to distinguish them.

His extended meditation on Litost (ask Google) is quite amusing in a Eurocentric way.

Trekked around Sydney CBD today, looking for stuff, more successfully than last time. The haul:

• A Macpac Nautilus tent from Paddy Pallin. It got a good review or two and seemed easy enough to pitch, at least with the help of the lovely young lass in the shop. One of those times when I went in optimistic (and well-researched) and it worked out well.

  Paddy Pallin are having a sale right now so I got it for $AU360 rather than the usual $AU450, bonus. Still seems a lot for two pieces of fabric, some pegs and two collapsible aluminium poles.

• A car-powered air compressor for air-mattress / lilo-type things.
• A mobile-phone charger for the car.
• Camping in Australia (Cathy Savage, Craig Lewis). This was more-or-less what I was after: locations and services, though the details are a bit sketchy. Lonely Planet seems surprisingly disinterested in the less kempt.

Now I just need all those little things: knives, forks, cups, pots, bog roll, ...

Finally got around to buying a domain: $AU33 for three years from the nondescript Website Domains registrar. So far, so unimaginatively kosher. I availed myself of the freebie DNS provided by EveryDNS; they're somewhat limited in the kind of records they'll serve up, but more importantly are apparently reputable.

At the moment I've got Apache running on Debian on my dear old P120 at home, so it's all terribly slow. I feared the 64kbits uplink would sour the deal but Blosxom blindsided me by taking several tens of seconds to render the index pages. perl, gotta love it.

DNS Report has proven useful for linting all that stuff.

...and my only excuse is that so many others have made the same mistake. To atone I present here law 11, so familiar to those who deal with modern universities:

The bigger the system, the narrower and more specialized the interface with individuals.

The most-recent edition has been renamed to The Systems Bible. I caved in and ordered a copy from Amazon. True to form, it won't be here until sometime in March.

I thought I'd try to tidy up a few things in Blosxom, such as the timestamps in comments, get the cookie memory-device going, that sort of thing. While the core and some plugins may be as-tidy-as-perl-can-be, the writeback (comments) one is pretty nasty.

I also tried to fix the formatting of the sidebar. Once again the lack of compositionality of HTML bit me on the arse: some things one can fix by twiddling some CSS in the flavour files, and others require a sift through the perl. To some extent it's a matter of code quality, but also there's the issue of what HTML objects are allowed with what combining forms. For example, the find plugin needs to return a form, so that'll be a div and not a span, thanks.

I guess my next trick will be some kind of functionalisation of my abbreviations plugin, so I can have some default text and also override it as needs be. Next Christmas, for sure.

The theme I pinched for Blosxom claimed to use an XHTML DTD, and so idly I thought I'd try to make it conform. Yep, a complete waste of time. I naively imagined that XHTML has twenty-first-century tech but in fact everyone's been ignoring it since 1999.

Both Safari and Mozilla seem to deal with it OK. I have no idea if any of this works in Internet Explorer, sorry.

There's a semi-usable packaging of the W3's validator available here. For dynamic content I use curl to grab the page then feed it through as a file. Not very convenient but the less lazy can script it.

I find it ironic that the motivation for XHTML in the Wikipedia article is to make things more anal, purportedly for an efficiency payoff. To my eye it's just XML buzzword compliance, an opportunity to clean up the semantics of the beast squandered on syntactic busy-work.

My pet peeve is that the layout rules are so damn complex when something as semantically simple as a bunch of markup combinators could fix this mess. This tradition in CS goes back at least as far as Henderson's 1982 paper on functional geometry and continues with Lava and pretty printing and many other works. Then, instead of spending an hour finding out that one should lay out a line right-to-left (perhaps, maybe, this week at least), I could just say "title beside search box" and get exactly that!

Heck, this would even be better than CSS: define a bunch of named objects and some way to lay them out explicitly. Completely separate content and presentation, perhaps even a "declarative" layout! Somehow the fundamental notion of compositionality has been MIA here.

A collection of short stories. I enjoyed Postcards from Surfers and Little Helen's Sunday Afternoon. Her closing The Children's Bach is the best piece of fiction I've yet read by her, but the standard Garner complaints of being a sketchy journal write-up and pedestrian-of-plot apply. Indeed, there are some parallels with Altman's Nashville. She describes Melbourne quite beautifully, though again I wonder how it would strike someone unfamiliar with the city. Her non-fiction has been more to my taste.

What a great piece of reportage from the Smage. I quote:

A court ruling has given the recording industry the green light to go after individuals who link to material from their websites, blogs or MySpace pages that is protected by copyright.

Of course they mean that the recording industry can go after people who link to material for which the recording industry owns the copyright. Repeat after me: there is one homogeneous recording industry, which speaks with one voice. Further down, the EFA says:

Dale Clapperton, vice-chairman of the non-profit organisation Electronic Frontiers Australia (EFA), explained the ruling as follows: "If you give someone permission to do something that infringes copyright, that in itself is infringement as if you'd done it yourself. Even if you don't do the infringing act yourself, if you more or less condone someone else doing it, that's an infringing act."

That's a bit strange; how can I give someone permission to infringe someone else's copyright?

Mr Clapperton added that this ruling could have wider implications for general search engines such as Google.

"What Cooper was doing is basically the exact same thing that Google does, except Google acts as a search engine for every type of file, while this site only acts as a search engine for MP3 files," he said.

But Ms Heindl said MIPI would not be going after Google in the same way it sued mp3s4free.net.

"Mp3s4free was different in the sense that it actually catalogued MP3 files that were infringing copyright material - Google doesn't do that," she said.

Hmm... it's good to know that Google doesn't index torrents... or perhaps pointers-to-pointers are OK. In any case this is precisely what the new copyright laws were predicted to lead to.

This application is just plain broken. It wants to be an operating system: from the look of Version 8 Adobe has tried to shoehorn most of the Mac OS X desktop into their proprietary web-browser-of-sorts. Hmm... perhaps this is what the Windows people have been dealing with all these years. unnecessary, unwanted feature-creep and integration.

The updater is broken. Just download the latest version. Oh wait, you need to get the "Download Manager" to download it for you. Grrr. And you sure do a lot of waiting on all these bloody programs... and then it tries to do the update thing anyway! Screw it, too much trouble.

Now, down to business: the instant-gratification eBook I rashly bought yesterday only lets me print 20 pages of it per month, which seems to me to be a strange compromise between the real world (fair use?) and what's possible with electronic authoritarianism. I found this mechanism is indeed easy to defeat.

A moment's reflection tells you that it is common (UNIX) courtesy for an application to only fiddle with stuff in your home directory, which you (of course) have free access to. (It could do nasty things if it's SUID or using OS DRM services, and that's surely in the post.) The hope is that by swapping some files we can reset the print counter, and that is indeed the case. On Mac OS X, simply, if inconveniently:

1. Kill Adobe Reader. I assume you haven't used any of your print quota.
2. Copy your ~/Library/Acrobat User Data somewhere safe. It seems to be a bit sensitive to a few things, so I suggest:

   cd ~/Library
   tar cfv ~/AUD.tar Acrobat\ User\ Data/
   

3. Fire up Adobe reader, print as much as you're allowed to.
4. Kill Adobe Reader, save the new state and extract the old:

   cd ~/Library
   mv Acrobat\ User\ Data/ /tmp/AUD.old
   tar xfv ~/AUD.tar
   

5. Go back to step 3.

If things screw up you can move your saved state back into place and things should work as they did before. The standard disclaimer applies to all of this: it worked for me, I hope it works for you, don't sue me if it doesn't.

I see I'm not the first to think of this.

I'm not at all sure things have gone as Laurence Lessig hoped with this eBook gambit; the one I bought seems to be loaded up to the gills with DRM with precious little thought given to usability and future-proofing. I've spent too long listening to RMS, I know.

More interesting is the question of whether I'm violating their copyright (rather than simply bypassing their DRM) by trying to print it. I guess I'd have made a copy, then, even if the digital original just sits there and bitrots until Adobe evolves to the point where it can't read it any more, or I buy a new computer or something equally inevitable.

According to the Australian Copyright Council I'm allowed 10% (in pages) or a chapter of the work, which comes out at roughly 20 pages, but no mention is made of a time period.

Also in that document is the curious:

If a book is no longer published, can I copy the whole book for my research?

Generally, yes. However, if you are aware that it is about to be republished within a reasonable time, it is unlikely you can copy the whole book.

Ah, I almost forgot — anything that limits your rights must certainly be a Technological Protection Measure, implying that futzing with it is probably a crime. I'm getting fonder of dead trees the more I read about this... so perhaps Rudd is right to sacrifice all those beautiful trees in Tasmania afterall.

I'm beginning to think I should have been a lawyer (or married one).

I've been trying to acquire a copy since reading an excerpt in the knowledge book with some intriguing assertions about general systems. Alibris has screwed me around twice but now someone has put it on the 'net.

• Unplugging the headphones makes it pause. Perhaps all iPods do this, but my iRiver didn't.
• The control is much better designed than my old iRiver.

• Some audible warning that it's out of juice. The little all-purpose LED glows red, I think, and that's that.
• A way to delete songs on the player itself, so I can fill it up with random crap and on-the-spot nuke the annoying stuff, rather than having to tediously go through it afterwards in iTunes at home.

• The dinky dock. My old iRiver had a standard mini-USB port, which happened to be the same as my Canon PowerShot A75. One cable was all I needed. Moreover I have no way to recharge it without having the iBook plugged in and running — there's no juice on the USB bus when it's suspended.

This book is linked from a lot of social-choice related pages on Wikipedia (a great way to advertise your book, for sure), covers an impressive selection of topics and got a good review. It's available as an eBook for $US20, or I could pay more, wait a month and get a dead tree from Alibris. What the heck, I think, how good can PDF DRM lockdown be these days?

I paid my money, Adobe Reader's iceberg functionality kicked in to download the book in a very mysterious way, and then crashed. No worries, I download it again, and this time it works. Not confidence-inspiring, and apparently eBooks.com has had plenty of experience on that score.

After futzing around with it for a while, the cons of the Digital Editions DRM become apparent. It seems to be locked to this machine. No other PDF viewer groks the file. The DRM-removing tools tend to not work for eBooks. Ultimately this means I cannot print the whole thing (which is as the publisher intends) or share it as one would by loaning the dead tree to someone. The pros are that one saves about a third of the cost and doesn't have to wait on the post, neither of which justifies such a loss of utility to me.

I trudged all over Sydney CBD today looking for a new pair of Docs and something that would let me recharge the iBook from the car. It seems the old Docs shop on Pitt St Mall has folded, and the joint down George St that for years proudly advertised cut-price Docs has gone for the factory- (China-) direct brand instead. I'd forgotten what a hassle it is shopping on the street.

Anyway, to cut a long ramble short, I ended up buying a "Powertech Plus Cat. MP-3463 3.5 Amp Universal Step-up DC/DC Converter for Notebook Computer" from Jaycar on York St for $40. The sealed-in cardboard says it was made in China and is distributed by Electus Distribution, and I can guarantee you that the cardboard was printed there too. I can't find it in either of their catalogues. There is also a 6 Amp version for those who have something hefty.

It works, with one small wrinkle: the iBook-sized plug adaptor is wired backwards! Fortunately the iBook is up to that game, simply ignoring a reverse-polarity 24 volts. The solution is to wedge the plug adaptor onto the cable backwards. For the curious these Italians have the details, or you can try to figure out what Apple is on about.

This proof is pretty straightfoward, but its implications are tricky to fathom. I tend to think that his notion of liberalism is pretty weird, and there's plenty of discussion on it. Again, while even Isabelle is convinced that the theorem is an analytic truth, there is plenty of doubt that Sen's mathematization is right.

For the keen there's an entire volume of Analyse & Kritik (1996 (18) Heft 1) dedicated to this topic. Eventually I hope to get around to looking at fellow Nobel laureate James M. Buchanan's criticism.

I've updated the document and also the darcs repo. Some linting, much more to do. Onwards! — to the Gibbard-Satterthwaite theorem.

At the Verona, with Jen. A freebie from Hopscotch via The Program. A fairy tale for adults, who would have thought. Beautiful, but the violence was a bit too graphic for me.

I tried to make some sense of it through the prism of Franco's Fascists versus the insurgents / freedom fighters / communists / concerned citizens but my history is a bit weak. I think the ending is supposed to imply Spain's reinstatement of the monarchy was broadly welcomed. Doubtlessly there were other allegories that I missed.

Smullyan's autobiography-of-sorts, or extended ramble through his interests. I quite enjoyed it, probably because I was fully prepared to indulge him, though it could have used a decent edit (quite a few typos). I don't think there are any new puzzles in this book.

On the side I've been chugging through Amartya Sen's classic Collective Choice and Social Welfare (1970), trying to convince Isabelle of some of the classic results in what is ultimately a theory of voting. As Richard Routley observes in his Repairing Proofs of Arrow's General Impossibility Theorem and Enlarging the Scope of the Theorem (Notre Dame Journal of Formal Logic, Volume XX, Number 4, October 1979):

The importance of a logically adequate proof is in no way diminished because, as it fortunately turns out, the theorem is correct under the intended (if often inadequately formulated) conditions. But that makes it easy to say that it is trivial to fuss over quantificational details of the standard proofs (proof failure comes ultimately in every case from quantificational errors, omission of necessary quantifiers or mistaken orderings of quantifiers, both major sources of invalidity in logic and mathematics) for every economist knows what is meant by the theorem, that it is essentially correct and its proof intuitively clear, and that a rigorous proof can be produced. The claim is false, as will emerge, even of the economic textbook writers. The textbooks have failed to produce what it is essential to have, especially in the case of a theorem with such far-reaching consequences (even if it is after all only an exercise in second-order quantificational logic), namely a correct and rigorous proof. The history of mathematics is replete with cases where what everyone was thought to know proved false, or where what was intuitively clear turned out to be mistaken or correct only under restrictive conditions.

In other words, perfect for formalisation in Isabelle.

At this point I have formalised the definitions given by Sen (and others) and shown Arrow's General Possibility Theorem (commonly known as Arrow's Impossibility Theorem) and the positive result about Social Decision Functions (SDFs). It's a huge space and there's plenty more to do.

arrows_theorem.pdf

A rough Isabelle-generated document of the development.

darcs get http://peteg.org/isabelle/arrows_theorem/

A darcs repository for the development.

Somewhat amazingly K.Rudd has managed to get Peter Garrett, my local member, onto his front bench as the environment and climate change spokesmodel. I find this slightly perplexing as Garrett is already a polarising figure, and modern politics is purportedly all about appealing to the middle in marginal seats, people who are probably worried that climate change will kill the last tree before they do. As the arts spokesmodel he looked harmless enough, and if they really wanted him for the greenie gig they could have parachuted him in after the election.

I hope I'm just being cynical here.

Take a gander at the political compass questionnaire. It's an oldie but a goodie. I come out as more libertarian than leftie by a small amount, though extreme in both directions. I'm not sure that's justified, given there aren't "I don't have an opinion on this one" options.

Somehow I ploughed through this book. Again, Garner is repetitive and so little changes from one angst-inducing event to the next that I lost interest in the questions she fails to answer, such as what she sees in the men she feels compelled to be with. (She says a lot about how she feels and how communication fails, but not much on the non-horizontal shared experience.) The characters that wander in and out of the narrative rarely have independent lives and few have any identifiable impact on the story, beyond being competitors for a man, or a man. Her engagement with junkies and drugs is drab and uninspiring, never failing to point out the obvious failings of each, while the transient benefits, the "why?" of her narrative, goes mostly unshared.

Historically this novel may be of interest insofar as it brings an Australian (if unenlightening and unerotic) bluntness to matters sexual and narcotic in 1977. Anne Summers must have seen a lot more in it that I did, in branding it the nation's best novel of that year.

I wonder if the Anglo fascination with the I Ching made it out of the seventies; Douglas Adams made hilarious use of it in The Long Dark Teat-Time of the Soul in 1988, so I guess it must have. (You can try an internet incarnation of Adams's version here).

These are the scripts for John Clarke and Bryan Dawe's recent 7.30 report shows on the ABC. Some are just plain funny but most serve better as keys to remembering the original interviews.

Tuesdays are give-us-ten-bucks-or-more at the Belvoir, downstairs at least. Even after the refurbishment that theatre remains a bit of a dungeon, serving as a home to their outre B Sharp company. The bar and ticketing area is all smiles and soft couches, and presumably it was all sweetness and light at the Keating! production upstairs.

This play is an adaptation of an apparently unique Latin novel. It rambles. Its not entirely coherent. Its ludicrous. Its quite long, at about three hours with three intervals. Well staged, well performed, though the macro narrative made merry with my empty stomach and eluded my grasp. It's terribly unsubtle, but what fun.

Another excellent collection of short stories from David Malouf. I especially liked Valley of the Lagoons, Every Move You Make, Elsewhere and the closing The Domestic Cantata. He's at his best in Australian settings, mining the coming-of-age and kitchen-sink drama.

mrak remarked, several years ago, apropos the author:

I only know her from the controversy over The First Stone. Feminists hate her like poison, apparently.

and I can see why, after reading it. A quick Google will turn up any number of snarky responses. I don't have a background in feminism and no real interest in the infighting, and as she herself says often here, the danger of overly codifying relationships is that the joy goes out of them. (A class of response seems to be that normal flirtatious interaction between men and women is fine... except when it isn't. Not such a helpful characterisation.)

Garner's prose is heartfelt and open, even as the central narrative is frustrated by a lack of cooperation. Her take on relationships, the university life and the stultifying effect of institutions (amongst other things) struck me as insightful and worthy of further development. I was a bit irritated by the repetition and the waiting-for-something-to-happen anecdotal structure, but I finished it in two sittings so I must be nickpicking.

Most of the workshop was quite technical, as I expected. Andrew Tridgell gave a good talk on his appreciation of the GPL, and Eben Moglen was quite amusing while arguing multifarious legal details.

Again it was free-for-the-unwaged evening at New Theatre. Similarly to the previous production I saw here, this one is slick and hilarious.

Quite entertaining, but watch out for those "it turns out that..."s. I would have preferred something that made the research accessible rather than this overly-simplified popularisation. At times they get ahead of themselves, using the technical terms "controlling for", "correlated" and "causal" for most of the book before giving a rough explanation.

Levitt's talk at TED is well worth a watch. Indeed, the economics of a Chicago drug gang is the best story in the book. (The effects of baby name choice bored me senseless.)

Ages ago, Jon lent me a copy of The Wire where a sound-test of Warren Ellis from the Dirty Three included some work by this Hungarian violin maestro. I couldn't find much on the net about him at the time, but now strangely enough, there are videos of him on YouTube:

(and, I note, some short samples of his work on his homepage.)

• An erratic compilation of old Ennio Morricone music scores.
• Jarvis Cocker's new album, imaginatively titled Jarvis. It's quite weird, somewhat like an Elvis Costello second-CD where he tries out all the kinds of music that didn't make him famous. Very endearing.
• Leonard Cohen: Ten New Songs, with the sublime A Thousand Kisses Deep (thanks to Dave for the pointer). Now I have to scare up I'm Your Man. I note that both he (a big man of words) and Raymond Smullyan (a big man of logic) were drawn to Zen.

  Even so, I can't get past the full version of the incomparable Waiting for the Miracle from The Future:

  Ah I don't believe you'd like it,
  You wouldn't like it here.
  There ain't no entertainment
  and the judgements are severe.
  The Maestro says it's Mozart
  but it sounds like bubble gum
  ...
  I haven't been this happy
  since the end of World War II.
  

  and so forth.

I hadn't been to the TAP Gallery for years, and it is was a review in The Program that brought me to this beaut production in the warmly embracing theatre, beyond an art-strewn corridor running beside the main gallery. Tuesday is their pay-what-you-can night, and I can't help but think a better policy would be a $10 bums-on-seats and a pass-the-hat-around afterwards.

The two blokes (Andrew Bibby and Rodger Corser) are fabulous, and Lotte St Clair is destined to become a Home and Away favourite. The drama is tight, fluid and mostly unaffected, founded in Andrew Bibby's heroic acting in the role of Dougie. Definitely worth seeing. Keep an eye out for their company, Ground Up Theatre.

(Just a small nit about Nick Marland's otherwise spot-on review: Sarah's father did not cark it in a mining accident, and the manner in which he did die plays the major part in the resolution of the fraternal friction.)

The CSIRO finally got a decision on the legitimacy of their wireless patent in the US, and perhaps it will solve their perennial funding crisis. As this is about hardware protocols I'm not altogether sure it's a terrible thing, being close to the original intended use of patents and all that. Anyway, I'm all for another Microsoft-esque tax on corporate America. Let's just hope they use it for more than beer and skittles.

Hosting a faux-News Ltd. general meeting in Adelaide, Murdoch uttered a whole string of things I more-or-less agree with:

• The tax system is a shambles. I think there's a greater need for clarity and fairness reform than a general decrease in rates, but still.
• The government surplus is somewhat useless, being, to my mind, really a John Howard re-election fund.

• Broadband internet in this country is crap. I don't know if the government should pay to improve the situation, but surely he's right to say that the crappiness will bite us on the arse in the long run. Our communications minister is unfortunately clueless on these issues; now it's not so much about availability as cost and quotas. As I say to anyone who listens, I used to pay $30 a month in Göteborg for a 100Mb/s connection connected to a gigabit-ethernet backbone with a traffic quota of 15Gb per day. Yes, you could and did pull eight megabytes a second on that thing. That was in 2004, and things can only have improved in Sweden by now.

  We may be the second fastest country in the OECD to take up broadband, but I'm sure every other country really did take up broadband.

• On Mrs Clinton, blue sky Madame President:

  "I can tell you she's running and I'd bet heavily on her winning the nomination but I wouldn't bet on her winning."

Who would have thought.

Beazley was stoked to have someone of import attacking the government, but as the big man's policy is to only back winners he couldn't expect a pat on the back himself.

(There's some more details at The Australian. Yes, he's trying to feather his own nest. It just so happens to be mine too, in this instance.)

I picked this up at the Westfield at Eastgardens. It's a mix of experimental movie noises and his sweeping movie scores.

Courtesy of Manuel.

I didn't know the story of the iconic American flag-raising photograph, so I found it riveting. Jock Alexander drew an apposite counterpoint back in 2004.

After finishing this book it struck me that it's helplessly Americentric; such giants of the field as Thierry Coquand and Gérard Huet, the entire COQ project, the notion of a "logical framework" (thank you Gordon Plotkin and friends), and sundry other influential things fail to rate a mention. (OK, Per Martin-Löf gets a guernsey as the godfather of neo-constructivism, though the entire Swedish-west-coast movement he inspired goes unremarked.) The problem of having to manually provide variable instantiations (due to the undecidability of higher-order unification) is alluded to (p270), but where is the follow-up pointer to the pragmatic resolution used in e.g. Isabelle, with linear patterns, stylised rules and all that?

The continual reference to the issue of proof and to mathematical practice as normative or indicative is misleading; the issue is how to engineer computer systems as rigorously as we do other artefacts, such as bridges and planes, and most of the epistemological issues involved are not unique to computer science. Similarly we need not think of these proof assistants as oracles so much as mechanisations of other people's expertise, in much the same way that structured programming and libraries (or even design patterns if you like that sort of thing) guide us towards best-practice, and employing algebraic structures leads to all sorts of nice things, like compositionality.

Putting it another way, why would one ever think that a computer system can be engineered to be more reliable than a motor car?

Still, the book does have some interesting discussions on just what a proof is. John Barwise's conception of formal proof as an impoverished subclass of mathematical proof rings true to me, though the particular example (p324):

... [C]onsider proofs where one establishes one of several cases and then observes that the others follow by symmetry considerations. This is a perfectly valid (and ubiquitous) form of mathematical reasoning, but I know of no system of formal deduction that admits such a general rule.

is a bit weak: in Isabelle, one could prove a case, prove that the others are in fact symmetric variants of it, then draw the conclusion. If the symmetry proof were abstract enough it could be enshrined in a library.

Purportedly his best book, and yet, at 470 pages, a solid third of that is flab. Things go well for the first half only to slow right down as the mysterious, inevitable, clearly flagged climax is delayed, put off, sent to fetch some cigarettes, have a pint and be disappeared for seven days by the AFP on suspicion of sedition (or perhaps horrorism). At best his facile humour is laugh-out-loud, and that holds for most of it.

Oh, the irritation, the irritation: John Howard on Lateline, putting up climatic strawmen. Paraphrased, symbolic gestures won't help, signing a piece of paper won't help, nothing will help except nuclear f'ing energy. (Does anyone else have a Denis Leary flashback?) I fear we're screwed until the last boomer carks it.

The show was redeemed somewhat by Martin Amis talking about his two-month-old essay The Age of Horrorism. (Could there be another writer more diametrically opposed to Islam's philosophy of modesty?) As always there's no real debate as neither Tony nor (to a lesser extent) the big man has any faith that the audience has a clue. He looked remarkably uncomfortable the entire time, almost as if he was in danger of sobriety. Watch out for the VODcast, email me if you're desparate for a copy.

(Aside: I'm reading Amis's London Fields (1989) presently, where he has a huge preoccupation with crappy and extreme weather.)

I stole this from Tim's shelf while he wasn't watching. I find it really patchy, perhaps because the main reason I picked it up was his potted history of proof assistants (Chapter 8). Here's some notes:

Chapter 6: Social Processes and Category Mistakes

I'm quite partial to James H. Fetzer's position that claiming computer programs can be verified is a category error. (I remarked to Kai a few weeks ago, self-evidently I thought, that proof at best assures us that our reasoning about an artefact is sound, and that the disconnect between what we talk about and the actuality of putting the artefact in the environment can only be bridged by testing, an issue our breathren in the empirical sciences have been ruminating about for centuries.) Note that I am firmly of the opinion that formal proof of just about anything is good if one can get it, the effort of comprehending what's being said aside. This is about the epistemology of computer science, of examining the so-rarely articulated general issues of moving from theory and practice.

My impression is that his position is dismissed (see, for example, this terse rebuttal by the usually erudite RB Jones) as being a category error itself; software-as-mathematical-artefact, hardware-as-physical-process, read-the-proof-to-see-what's-proven. In context here, though, Fetzer's claims are set against the blue-eyed optimism of those who want to make the correctness of their system contingent only on the laws of physics (p236):

"I'm a Pythagorean to the core," says Boyer, "Pythagoras taught that mathematics was the secret to the universe." Boyer's dream — not a hope for his lifetime, he admitted — is that mathematical modeling of the laws of nature and of the features of technology will permit the scope of deductive reasoning to be far greater than it currently is. "If you have a nuclear power plant, you want to prove that it's not going to melt down ... one fantasizes, one dreams that one could come up with a mathematical characterization ... and prove a giant theorem that says 'no melt-down.' In my opinion, it is the historical destiny of the human race to achieve this mathematical structure ... This is a religious view of mine."

Unusually for me I'll say no more until I've read Fetzer's paper.

Chapter 8: Logics, Machines and Trust

• MacKenzie doesn't say anything much about the logic employed in PVS; this is another point of departure from the Boyer-Moore theorem prover (beyond the approach taken to automation). My understanding, from Kai, is that it uses a version of higher-order logic.
• Cute: there's a "mathematically natural" example of a statement that is true but does not follow from the Peano axioms (cf Gödel incompleteness). Check out the Paris-Harrington theorem.

More as I get around to it.

At the Verona. I also signed up for their movie club: it costs $12 for a student, you get two free tickets per annum and the ticket price drops to an unbelievable $8.50 for oneself and one's friend. I'll make that money back in a month.

Took me a while to get through this one. Barry's writing style is a bit opaque, and the dry humour is welcome but unfortunately sparse. He has a tendency to explain his experience by referring to others', and then omitting concrete descriptions for those of us unfamiliar with his references. The book overflows with a self-aware immodesty, and the publisher's gamble is that the paying readership will indulge him on the basis of his historical place in the nation's bosom.

The last chapter is quite out of place in an autobiography, being a commentary on the post-reason, post-Enlightenment politics of 2006. Good to see John Quiggin get a guernsey though.

I scored some free tickets from The Program. First time at the Ensemble Theatre, a tiny theatre on quite a pretty little stretch of the harbour at Kirribilli. Met up with Jen at Milson's Point train station and had a drink at what seems to be the only pub in the area; it pulls a strange cross-section of punters, that's for sure. We had a quick dinner at Luigi's (Italian, in the hub of restaurants) and hurried down the backstreets to be there just in time.

The play itself was a pretty standard exploration of themes surrounding relationships, e.g. as listed in this review in the Smage. I found it stultifying for extended periods, though the actress provided great relief whenever she was on stage. I just can't imagine too many new things to be said in this format, and a retreat to novelty as happens here is a bit of a cop-out. The social upheaval in Argentina over so many years could surely yield something more than this.