PLDI 2016
I just got back from the 2016 Programming Language Design and Implementation (PLDI) conference (my first PLDI!) in Santa Barbara, along with the Programming Language Mentoring Workshop (PLMW). I met a ton of great people in the PL community and even snuck in some good talks.
PLMW
First: PLMW - a day-long mentoring workshop designed to introduce new grad students and senior undergrads to programming language design and implementation. The workshop was divided into two types of talks: advice and research, along with some ice-breakers to get to know the other attendees. The advice was generally good, even if not particularly novel from my perspective (most other attendees hadn’t worked in industry for an extended period). Steve Blackburn’s talk on Empirical Evaluations was basically Emery’s Research Methods class condensed down to 20 minutes. To summarize it down even further: empirical research must be clear, honest, and reproducible. Kathryn McKinley emphasized that research takes place in a community, and that communicating, collaborating, and building relationships are integral parts of research.
It was fun to hear about Matthias
Felleisen’s Racket-related
research, and how the focus has shifted over a 20 year timeframe, on to
the current work on Typed Racket and gradual typing. On the research
side, I was especially excited by Armando
Solar-Lezama’s talk on the
program synthesis state-of-the-art, and how synthesis interacts with
verification and machine learning. James
Bornholt’s talk on
Uncertain<T> was also neat - there are definitely APIs I’ve used
where I would have loved to get a point estimate paired with an
explicit probability distribution.
PLDI
There were a number of fun talks I attended, so I’m just going to mention a few highlights. Rehearsal (PDF) is Rian, Arjun and Aaron’s work from our PLASMA lab, which is able to find configuration bugs in Puppet by deriving formal semantics for Puppet programs. It verifies that manifests are deterministic (the manifest results in a single possible state of the system), and idempotent (the second, third and so-on runs have the same effect as an initial puppet run on a fresh machine) by feeding these checks as formulas to solve into an SMT solver. Its great to see formal techniques applied to the messy area of devops and configuration management. Not only were the results great and very relatable, but Arjun’s presentation was excellent.
While not a conference talk, I had the pleasure of talking with David
Tarditi, who
is leading the MSR
CheckedC
project to enable developers to write safer C code. I’m a big fan of
incremental language and runtime extensions, as rewriting everything
in new, safer languages like Rust or Go isn’t necessarily practical or
desirable. It looks like there are a number of open research
questions
that have to do with CheckedC, and I’ll definitely be taking a closer
look over the next few weeks. I’ve already started converting my
libsd project as a
way to get familiar with the spec and syntax.
The Jacqueline Python Web Framework
My favorite talk of the conference was Jean Yang’s “Precise, Dynamic Information Flow For Database-Backed Applications”, and not just because her running example involved Arjun and Emery:
Web services intrinsically manage access to private data based on user identity. Permission checks are hard to get right, and end up peppered all over the place if you’re not disciplines. The authors use programming-language techniques like faceted evaluation and formal semantics to provide strong security guarantees underneath an extension of the Django framework in Python! This is another thing I hope to try out and experiment with soon.
Overall, it was a great experience, and left me fired up to get back to research here.