Some notes from SPLASH 2015

Last month, I headed to Pittsburgh for SPLASH 2015. Sadly, the trip was brief, since I had to leave the conference early to make it to a friend’s wedding, but aside from my own talk at SPLASH-I, I managed to catch several other SPLASH-I talks, chair a session at Onward!, participate in a lively panel discussion, and throw a practice talk party in my hotel room. A few themes emerged from the smattering of talks I saw at SPLASH: domain-specific languages, “end-user programming”, a blurring of the distinction between dynamic and static languages, distributed programming, and program synthesis – all topics of interest to my group at Intel Labs.

A few SPLASH-I talks

SPLASH-I was a track of talks by industry researchers and practitioners. Here are a few highlights:

• Josh Watzman from Facebook gave a talk on Facebook’s transition from vanilla PHP to Hack, their optionally-typed dialect of PHP. I saw some similarities to Sam Tobin-Hochstadt’s work on occurrence typing. However, most of the talk was not about technical matters but about the social and cultural challenges of getting the whole engineering organization on board with the transition. One thing I would have liked to hear more about was their later open-sourcing of the system, but instead the talk pretty much ended with when they finished converting the code that runs Facebook to Hack, around the end of 2013.
• Tom Van Cutsem of Bell Labs gave a talk on the newest ECMAScript standard. His talk reviewed some ECMAScript history and introduced some of the new features in the 2015 standard. The ECMAScript 4 standardization process, which tried to add a lot of new stuff to the standard at the same time as cleaning up the existing stuff, was abandoned in 2008; it was followed by ECMAScript 5 in 2009, which focused on standardizing the small core semantics of the existing language rather than adding lots of new features. Now, in 2015, we finally have ECMAScript 6, which expands on that small core semantics. ES6 has classes and modules, but to me, the most interesting new features are generators and promises, which can be used together as an alternative to callbacks. There’s also lots of other new stuff in ES6 that the talk didn’t have time to cover in detail. Browser support for ES6 is still kind of spotty but improving all the time, and there exist tools to compile ES6-compliant code to something that current browsers can understand.
• A couple talks at SPLASH-I focused on “end-user programming” for business applications. The one that I saw was “Model, Execute, Deploy: Answering the Hard Questions about End-user Programming”, presented by Shan Shan Huang from LogicBlox. Her talk focused on end-user programming for the enterprise software market. There were some sobering statistics about how often enterprise software projects fail to address the needs of the people they’re built for (bookkeeping and organizational planning, for instance), necessitating the need for end-user programming. Shan Shan used the phrase “relational bidirectional computing” for looked to me like spreadsheet-style or dataflow-style programming. Although I didn’t get a great sense of what it would be like to use the LogicBlox query language to solve real problems, it does seem like one advantage over SQL is that it gets rid of the “table” abstraction, or at least doesn’t expose it to the user. Instead, users can write constraints that describe the data they want to see; they don’t have to think about which data might be in which tables with which other data.

There were lots more talks at SPLASH-I (including mine), and slides or video are now available for many of them.

A few Onward! talks

This year, I served on the program committee for Onward!, a conference that aims to be “more radical, more visionary, and more open than other conferences to ideas that are well-argued but not yet proven”. I saw several interesting talks at Onward!, both in the session I hosted and in other sessions. Here are three of them:

• Shaon Barman of UC Berkeley presented his paper, “Toward tool support for interactive synthesis”. Program sketching has been a little mysterious to me for years, but after seeing Shaon’s talk, I feel I have a better grasp of it. A sketch is a program with holes in it, and synthesis by sketching means starting with a sketch, plus a hole-less reference version of the program that we know is correct. Then, we synthesize code to fill in the holes in the sketch to match the semantics of the reference implementation (but presumably with some advantage, like being faster). The challenge of synthesis by sketching is that the less specific the sketch, the larger a space of programs we have to search. But, if the programmer has some insight, say, that a computation can be decomposed into two independent computations, we can cut down the search space considerably by using a sketch that has two holes in it instead of one. Although I didn’t understand all the details, the idea of Shaon’s work is to offer tool support for the discovery of this kind of sketch “structure”. The paper is available.
• Sylvia Grewe of TU Darmstadt gave a great talk on her work on “Type Systems for the Masses: Deriving Soundness Proofs and Efficient Checkers”. A type system is sound if, when a program is well-typed according to the type system’s rules, it will not produce run-time type errors. How to automatically verify that a nontrivial type system is sound, though, is a hard problem in practice. Moreover, even once we know that a type system is sound, we don’t know that the type checker actually implements the specification set forth in the typing rules, and an implementation automatically generated from the rules is likely to be impractically inefficient. This paper lays out an ambitious proposal to address these problems. The authors have implemented a tool that lets you specify a language, including syntax, evaluation rules, and typing rules; from this specification, you can use the tool to semi-automatically generate a proof of soundness of the type system (using an automated theorem prover together with some domain-specific proof strategies that the authors developed) as well as an implementation of a type checker that is more efficient than one implemented directly from the rules. Their code is on GitHub, and the paper is available.
• Alex Prokopec of EPFL presented his work on “Isolates, Channels and Event Streams for Composable Distributed Programming”. “Isolates” are a new family of abstractions for distributed programming as an alternative to the actor model. Isolates are processes that send and receive events on channels. The key innovation over actors seems to be that each isolate has a set of internal event streams, one for each channel that the isolate owns. Because different event streams are kept separate from one another, events on different channels don’t interfere with each other, making it straightforward to run separate protocols at the same time. An example is a cache that has to act as both a server and a client. My understanding is that the way people work around this two-protocols problem today in actor languages like Erlang is by “tagging” messages as belonging to one protocol or another, but this is kind of an ugly and ad-hoc solution and easy to get wrong. The paper has a series of examples culminating in a CRDT implementation.

Unfortunately, there only seem to be videos available for a handful of Onward talks, and not for any of these.

“The Future of Programming Languages and Programmers”

Finally, while at SPLASH I served on a rather grandiosely-named panel. The other five panelists were Lars Bak, from Google, known for his work on V8 and Dart; Nick Feamster, a Princeton professor who works on networking and security; Rob DeLine, from Microsoft Research, known for his work on human factors in software engineering; Crista Lopes, a PL and software engineering professor at UC Irvine; and Peng Wu, director of the Programming Technologies Lab at Huawei Research. I was by far the most junior person on this panel!

Much of the audience-question-driven discussion centered around DSLs and the idea of “programming for non-programmers”. For the most part, the other panelists agreed with me that “programming for non-programmers” is an oxymoron, and that programming in a DSL is programming. Peng asked rhetorically, “If one person implements a numerical algorithm in MATLAB, and someone else ports it to C++ for efficiency, then which one of them are we going to claim is the ‘real’ programmer?” Nick said he envisions a future in which network engineers are programmers, although perhaps with a different set of skills than what we think of today as being essential for all programmers to know. For example, a language for network engineering might not have for loops and might not even be Turing-complete. (His keynote talk at SPLASH touched on the same themes.) I pointed out that I see Turing-completeness as a red herring anyway; after all, we wouldn’t claim that people who program using non-Turing-complete dependently typed languages like Agda aren’t “really” programming. Sooner or later I think we might see more language designers try hard to avoid Turing-completeness, or at least not make a point of building it in on purpose.

No recording was made of the panel, but Steven Fraser, the organizer, is planning on writing a summary of it for later publication. You can also read the brief position statements that each of us were asked to write.

OOPSLA

Of course, the best and most important part of any conference is getting to meet and catch up with lots of researchers from all over the world. This is often best done outside of official conference events. OOPSLA is the flagship event of SPLASH, but instead of attending any official OOPSLA talks at all, I hosted a practice talk party in my hotel room. I suspect I got a lot more out of the talks that way anyway, because the speakers and listeners all ended up having a friendly extended conversation, instead of having to wedge our questions into a confrontational five-minute Q&A session. Thanks to Stephan Brandauer, David Darais, and Kyle Headley for participating in this experiment! Let’s do it again at the next conference.