OOPSLA: Student Research Competition

One of the most interesting things I did at OOPSLA was be one of the three judges for the ACM Student Research Competition. A while back we refereed 20 paper submissions, which we narrowed down to 7. These 7 had posters in the OOPSLA poster session. From these 7 we narrowed it down to 5 who gave the judges a 10 minute presentation with 5 minutes of questions. After that the judges had a very spirited debate to decide on the following:

• 3rd place "Activating Refactorings Faster" by Emerson Murphy-Hill.
• 2nd place "Flexible Ownership Domain Annotations for Expressing and Visualizing Design Intent" by Marwan Abi-Antoun.
• 1st place "Code Genie: A Tool for Test-Driven Source Code Search" by Otavio Lemos, Sushil Bajracharya, and Joel Ossher.

Congratulations to all of these students. We had a very difficult job deciding the positions. The quality of all the posters and presentations was extremely high - I don't think any of us (the judges) expected quite such a wonderful show! This shows that some of the very best students are broadly in the OOPSLA field, which is a very healthy thing for OOPSLA.

Thanks go to Nadyne Mielke for organizing the competition.

OOPSLA: Brian Foote "big balls of mud"

Lots of people have mentioned to me the Big Ball of Mud paper. It's a classic apparently.

One of the authors, Brian Foote, gave a keynote at OOPSLA. I'm afraid to say I found it deeply disappointing. The talk - which lasted ninety minutes - really had very little to say, other than repeat the BBoM thesis (this really only takes a few minutes to describe). Given that the BBoM paper is now ten years old now I was hoping to see what the speaker had learnt given these ten years: were things better or worse? What have we been doing right? What more needs to be done? Should we give up? Or is there some new research area waiting to emerge?

None of these questions were answered. Although the talk was mildly entertaining with creative use of powerpoint and stories, I didn't feel that it was appropriately technical enough to end an OOPSLA. Shame. Sorry, Brian.

OOPSLA: Ownership session

3 very interesting talks on ownership:

1. Inferring aliasing and encapsulation properties for Java by Foster/Ma
2. Multiple ownership by Cameron/Drossopoulou/Noble/Smith
3. Ownership transfer in universe types by Mueller/Rudich

I especially enjoyed Nicholas Cameron's talk: he has his mojo (sic)! They use an interesting form of existential over ownership annotations (written using a wildcard syntax). I wonder if you could encode their stuff into sep logic where their o&? constraints would be encoded as EXISTS b.o&b formulae? At the very least it would provide some sort of semantics. Yet another thing to discuss with James Noble!

OOPSLA: Second Life/LSL

I must now be the coolest person in MSRC. I went to William Cook's tutorial on Linden Scripting Language (LSL) so I have now written some LSL scripts!!

Possibly more impressive - in terms of street cred - I did have breakfast and a lengthy chat with Babbage Linden. He's driving the Linden Labs effort to migrate to mono (.NET on Linux). Super cool stuff. Wow.

OOPSLA Panel: 40 years of languages

[Grrr...the hotel wireless is dying under the strain of several hundred oopsla attendees attending to read email. I wrote a lengthy piece about the panel, but after clicking the post button, my machine lost its connection and I lost the blog entry. Damn.]

On the panel were Guy Steele, James Gosling, Betrand Meyer, Anders Hejlsberg and Ole Lehrman Madsen. It was quite interesting. The panellists got five minutes to talk about the influence of Simula 67 and the future of PL. Highlights:

Steele: He quoted Alan Perlis quite amusingly. He also stated that there would be more functional programming in the future but you can't hide state everywhere. He was still worried about the 5% of state manipulating glue.

Gosling: He had an early job maintaining a Simula 67 compiler. He spoke about "drivers" for languages. For Java it was the network. He also mentioned in-memory databases [I've been talking about these recently - I'd like to work some more on these as I think they're going to become very important.]

Meyer: He promoted Eiffel (of course). He mentioned that people still used imperative languages because Hoare and Dijkstra had provided us such great reasoning tools. (ha!) He urged people to look at the concurrency model in Eiffel.

Hejlsberg: Anders spoke about the growing importance of functional programming in the context of multi-core. He mentioned the (wonderful) news of the productization of F# by Microsoft.

Madsen: Ole spoke about the importance of history - people should know more about what has been done in other languages.

Some further points arising from questions from the floor:

1. On functional programming:
Bertrand: FP is good but won't take over. We have to reconcile Angel and Beast. Hoare told us how to reason about messy imperative languages.
James: problem with FP is that it's too difficult. Humans are imperative.
Guy: More FP in future, but never 100%. Big problem is state - what about the remaining 5% code that shifts state around?

2. Can we change programmers through language?
MEYER: nice features of Eiffel: type system and pre/post/object invariants
OLM: teach higher level stuff. Not endless discussions about e.g. multiple inheritance. Should learn from other fields - no more "XXX extensions of Java"
GUY: What about PL features to boost programmer's self esteem? :-)
[Gosling: Isn't that what Perl's about?]

3. Is OO necessary but not sufficient? (Quote from Nygaard)
OLM: Teaching too technical - COOL. Simula closed world - need more, e.g. distributed programming, global ubiquituous programming. Time and location now matter.

4. Is programming hard?
GOSLING: Boeing spend 3kdollar per line because its so hard to reason about code. (And its assembly code)

5. Meta programming?
ANDERS: Meta programming is what makes Ruby nice, not lack of types.

6. Why dont we have co-routines a la Simula? (And build other concurrency primtives on top of it?) ANDERS: Never going to be a single model of concurrency.
GUY: Fundamental commitment to stacks is the enemy of concurrency. (They give an ordering)

oopsla 2007

I'm attending OOPSLA 2007, which is in Montreal, Canada. I have a paper in the "language specification" session of the research track. It' s a huge conference and there are a huge number of talks/tutorials/workshops to attend at any one time. I'll blog what I attend if possible...

F# productization

Finally one of the most exciting pieces of news is out. Today it was announced that Microsoft intends to productize F#! F# is a functional language originating from the ML family (actually it's a close relation to OCAML) that was designed to be .NET language. It was designed and implemented by my colleague Don Syme in MSRC. Many congratulations to Don who has worked incredibly hard to get F# to the stage where it can be transferred over to the product team.

OOF not OOO

I've finally solved one of the Microsoft mysteries. No, not that one! Inside Microsoft people abbreviate the phrase "Out of office" as "OOF". In my three and a half years here I've not found anyone who could explain it. Catching up with Nadyne's blog, I've now discovered what it means. Somehow I feel better for knowing - I should get out more often I guess!

SQL code injection joke

A nice cartoon highlighting one of the problems addressed by Cw/LINQ can be found here. [Thanks to Nick Benton for spotting this!]

Zune 2.0

It's a tough time to be considering to buy a media player it seems. Everyone's seen the new Apple devices. Somewhat drowned in the noise, Microsoft also upgraded the Zune. There's a nice video here. Still single-touch, not multi-touch, but a much improved UI.

Mateja in the news!

My wife, Mateja Jamnik, was in the news last week in Slovenia. She attended a congress for Slovene scientists who work abroad. She ended up being rushed into the TV studios and being interviewed live on the 10 o'clock news - Odmevi - which is a very big TV slot in Slovenia.

If your Slovene is up to it - you can view the interview on the web. Go to this page and click the archive for 4th October 2007. This will launch a pop-up with an emedded player. There's about 3 minutes of introduction before you get to Mateja! What a star!

C# overloading

I just discovered an interesting "slip" in our ooPSLA paper. (Actually it's not a slip in the fragment of the language we consider, but it's dishonest in the Parnas sense (see an earlier blog entry)). I'm grateful to Eric Lippert for pointing this out to me.

Consider the process of typing a method call: e.m(f1,f2).

• First we synthesize a type for e, call it sigma.
• Next we generate a set, call it CMG, of all the candidate methods, i.e. the methods called m in sigma and its supertypes.
• Now we need to discover which one of these candidates are applicable: this amounts to checking that they have the same number of arguments as supplied (in this case 2), checking the modes (to handle ref parameters), checking that the arguments f1, f2 can be implicitly converted to the candidate argument types(*). [I'm ignoring generics here. If the method is generic and the call does not provide an explicit type argument list, then we need to use type inference to infer the type argument list]
• Finally we take this set and determine if there is a best method signature. [This is the heart of overloading resolution.]

Or that's what I thought happens! It turns out the last step is not strictly speaking true!!! It should be:

• Finally we take this set and the argument list and determine if there is a best method signature.

The problem arises because C# lets you define your own (cyclic) implicit conversions. Imagine we have two classes X and Y (that are not subtype related) but we define implicit conversions in both directions. Then imagine we have overloaded methods:

static void m(X x)
{
Console.WriteLine("Picked Program::m1");
}
static void m(Y y)
{
Console.WriteLine("Picked Program::m2");
}

and the code:

X x = null;
m(x);


C# picks the first "m" method because its the best match for the argument given that we know that argument of static type X. So overloading resolution needs to use this static type. As not every expression can synthesize a type, we have to pass the argument itself. If we had just considered the type signatures of the method m (i.e., X -> void and Y -> void) then neither would have been better and we would have rejected this call as ambiguous. Ha!

I'm currently extending our ooPSLA paper into a journal version. Part of this is formalizing the overloading process in C#. (It has been extended for C# 3.0 - it treats delegate types in/co-variantly.) Hence why I tripped over this.


(*) For some reason in the camera-ready copy this type check got missed out! Sorry - it was in the submitted version - I must have been too enthusiastic with my CTRL-ks when preparing the camera-ready copy :-(

POPL 2008

The paper with Matthew Parkinson on using separation logic to verify OO programs with inheritance got accepted for POPL 2008. Hurrah! We're currently working on an extended version that we should release in the next couple of months.

See you in San Francisco in January?