Looking Out To Sea

I’m just back from the Edinburgh Cafe Sci with Philip Wadler as speaker.

The evening started with Ed giving a welcome to everybody and explaining what the standard procedure is: a short talk, a break for drinks, then some questions.

Then Philip Wadler stood up and introduced himself as working in the field of computer science, a name with only two problems — the emphasis on technology suggested by the word “computer” and the desperate plea for relevance that calling yourself a science seems to imply! He then said that his aim for the evening was to argue that there is depth to computer science that has nothing to do with the job of IT support.

He started with the basics of logic, in the study of rhetoric founded by the ancient Greeks. He asked everyone to do a short experiment — in fact, two different statements of the famous Wason card problem — as a demonstration of the power of logic and also its usefulness in even the simplest setting.

Having demonstrated that logic probably isn’t all that bad after all, he started a brief history of 19th century logic. George Boole invented a calculus of logic, to the delight of Leibniz (who I think was dead by then, but probably felt vindicated all the same). Frege came in later, someone whose name I didn’t catch (Gensen?) and then onto Church and the lambda calculus. Finally, he explained that many of these proofs and reinterpretations were shown to be equivalent.

It’s hard, very hard, to get across the beauty of things like lambda calculus to anyone, never mind the drinking patrons of a cinema bar, especially when you have no overhead projection facilities. I’m impressed Philip Wadler held everyone’s attention for so long, though inevitably there were some points where the focus began to waver. I think he suffered from lack of preparation, to be honest.

After the interval the questions were quite mixed. There were a couple on the competing language paradigms and the apparent lack of inroads that functional languages have had in the Real World™. Some guy (okay, I say “some guy” but it’s the same tedious guy every time) wanted to argue that logic wasn’t universal but I think any evidence he might have had was self-refuting. Gödel was touched on, and the fascinating but subtle topic of incompleteness and inconsistency. He got in a plug for research people are doing at Edinburgh into proof-carrying code. And he also highlighted that Scotland is the home of two important functional languages (or families), ML and Haskell. And maybe I’m not being true to my East coast roots here, but I prefer Haskell. :-)

If you couldn’t make it, or want more Wadler goodness, I recommend this Google Tech Talk on “Faith, Evolution and Programming Languages”.