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.
A freebie courtesy of the Darlinghurst Theatre, at the Dendy Opera Quays with Jen. In the style of Dogville, sans Nicole Kidman.
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 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.
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.
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.
