peteg's blog

GPLv3 Workshop at the Cyberlaw Centre.

/cs | Link

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.


/noise/movies | Link

/hacking/mac | Link
André pointed out Terminator to me, a cross-platform terminal emulator written in Java. It sounds promising; the only things tying me to are XEmacs, a DVI viewer and xterm.

/noise | Link
Back in 2004 I went to Stockholm with my Mum, and somehow picked up the idea there was an ABBA museum in that city. It seems I had just got a bit ahead of myself.

/noise | Link
Iemma tries to stitch up the Martin Place geek vote by promising free wifi in central Sydney on the never-never (beyond the next election). I wonder how they'll make this fly; my expectation is a Windows-only port 80 effort.


/noise/movies | Link
A freebie courtesy of the Darlinghurst Theatre, at the Dendy Opera Quays with Jen. In the style of Dogville, sans Nicole Kidman.

/noise/beach/2006-2007 | Link
Noonday swim at Gordon's Bay. Not as hot as the BOM's forecast led me to expect.

/noise/beach/2006-2007 | Link
Swim in the early afternoon at Gordon's Bay.

New Theatre: Laughter on the 23rd Floor

/noise/theatre | Link

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.

Steven D. Levitt and Stephen J. Dubner: Freakonomics

/noise/books | Link

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.)

Leonard Cohen: I'm Your Man

/noise/movies | Link
The songs are great but the performances tend not to be. It's a shame they didn't just make a straight documentary on the big man. There are plenty of thoughtful comments at IMDB.

/noise/beach/2006-2007 | Link
Swim in the late afternoon at Gordon's Bay.

The Prestige

/noise/movies | Link
At The Ritz.

/noise/beach/2006-2007 | Link
Swim around 6pm at Gordon's Bay.

/noise/beach/2006-2007 | Link
Early-evening swim at Gordon's Bay. Oh yes, if you want to go snorkelling in Sydney then that's the place to go... and Clovelly, and Little Bay.

Félix Lajkó: YouTube to the rescue.

/noise/music | Link

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.)

Napoleon Dynamite

/noise/movies | Link
A sort-of halfway house to Todd Solondz's excruciating oeuvre (specifically, Welcome to the Dollhouse).

/noise/beach/2006-2007 | Link
Quick dip at Gordon's Bay late in the afternoon. While it was hot around noon, the wind cooled things off by the time I got there.

TAP Gallery: Below

/noise/theatre | Link

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.)

New Music

/noise/music | Link
Got my order from Chaos:
  • 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.

/noise/beach/2006-2007 | Link
Quick late-afternoon swim in a surprisingly cold Lake Coogee. The place is filling up with accents. Incredibly flat surf.

Easing into the 21st Century.

/hacking/mac | Link
Met up with André in Newtown for a coffee and some lunch, and being the unpaid ambassador for Apple that he is, we ended up in the Apple store on Broadway and I parted with $119 for an iPod Shuffle, a replacement for my venerable 256Mb iRiver iFP-390T I bought in Boston at the end of 2003. I can't see why it needs an on/off switch.

Who Killed the Electric Car?

/noise/movies | Link
With Rob at the Verona.

The Zero Effect

/noise/movies | Link
On Dave's recommendation.

/noise/beach/2006-2007 | Link
Big trek over to Centennial Park for a coffee and newspaper perusal, then off to Gordon's Bay for a lazy late-afternoon paddle. A beautiful day in Sydney, supposedly 22 degrees and dry enough not to raise a sweat.

CSIRO's wireless patent.

/cs | Link

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.

Rupert Murdoch: putting the boot in.

/noise/politics | Link

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.)

Asimov: The Caves of Steel

/noise/books | Link

/noise/beach/2006-2007 | Link
Quick swim at Gordon's Bay in the mid-afternoon, trying to beat the rain. (It didn't show up until nightfall.)

Lucky Number Slevin (The Wrong Man)

/noise/movies | Link
Late afternoon screening at The Ritz with Jen.

Asimov: The Naked Sun

/noise/books | Link

Dijkstra: Under the spell of Leibniz's Dream

/cs | Link

Courtesy of Manuel.

Flags of our Fathers

/noise/movies | Link

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.

Jock Alexander's The war in Iraq

/noise/beach/2006-2007 | Link
Quick late-afternoon swim at Gordon's Bay, as the front passed through.

Ennio Morricone: Crime and Dissonance

/noise/music | Link

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

Asimov: I, Robot

/noise/books | Link

/noise/beach/2006-2007 | Link
Went snorkeling with Rob at Camp Cove, from the beach there, along the rocks, around to (the infamous nudist) Lady Bay Beach on the harbour side of HMAS Watson. Got a bit sea sick after a while, and there were heaps of little white jellyfish in the water. Beautiful day for it.

/noise/beach/2006-2007 | Link
Quick swim at Gordon's Bay after work, at 6:30pm.

/noise/beach/2006-2007 | Link
A dangerous surf warning sent me scurrying to Gordon's Bay. Full of crap after the recent rain, more bluebottles than I've ever seen strewn on the beach.

/noise/beach/2006-2007 | Link
Tried swimming at Coogee with Ben (up here for APLAS) but it was too rough. Off to Gordon's Bay for us.

Wallabies v Wales: 29-29 at Millenium Stadium (Cardiff).

/noise/sport | Link
What a fiasco, a 29-all draw. The Welsh number 13 is a magician. Playing Giteau at number 9 was a bad move. Larkham came off sometime around the 60 minute mark rubbing his shoulder, so it may yet be holidays for him. Latham was the only back to shine.

Donald MacKenzie: Mechanizing Proof II

/cs | Link

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.

/noise/beach/2006-2007 | Link
Again, too many bluebottles for me at Coogee, circa 5:30pm. A dripping Scotsman promised me there were plenty out there, that the sting lasted for but a wee minute. I figured that Gordon's Bay was worth a try, and so it was, even if there's not much happening without the snorkeling accoutrements.

Martin Amis: London Fields

/noise/books | Link

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.

Andy's On-line Self-Help Call-for-Help.

/noise/blogging | Link
The problem with a public blog is that is has to be interesting, or it languishes, as this one does, reader-less, apart from the odd Google misfire that sends people looking for the best seat in some Ticketek venue this way. At the end of the night it's hard not to verb the noun, not to non-sequitur. Others are voluble so that I may be taciturn. Andy, who apparently runs a plethora (or perhaps a cliché) of blogs, appears to be outsourcing the authorship of his self-help book.

/noise/beach/2006-2007 | Link
Aborted the circa-5:30pm swimming attempt due to bluebottles. Truckloads on the sand, at the edge of the receding tide. I'm way too blind to play that game.

Donald MacKenzie: Mechanizing Proof I

/cs | Link

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.

/noise/politics | Link

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.)