A Very Brief SPLASH Writeup

Sup nerds!

Last week the SPLASH conference— the main academic conference for programming language research— came to town. I decided on a whim to buy a ticket and go.

It was definitely a different experience than an industry conference! Each slot was 3-4 papers back to back, followed by questions on all of them at once. Most of it went over my head, given 1) it's an academic conference and 2) it's in a field I barely know. So I don't think I got out of it as most attendees, but I'm still glad I went.

Also I was the only person without a university affiliation. That was a great conversation starter.

So here were some the talks I went to! Headers link to the sessions

Natural Language-Guided Programming

When you start using a new API, you need to learn all of the methods and calls. You know what you want to do but not how to do it. The authors built a tool which reads comments and outputs code snippets that use the API properly, like putting in # get foo.csv and having it give back df = pandas.read_csv('foo.csv', delimiter=',').

They did this by training GPT-2 on public Jupyter notebooks. Training on notebooks without high-level comments produced worse predictions than models with them. Interestingly, grabbing random methods and including samples of their docstrings produced predictions almost as good as using human comments. Possibly a sign of how well-documented the core python ecosystem is.

At the very end they talked a little about Copilot and Codex. I got the impression they did most of their work independently and were as surprised as everyone else when those came out. I imagine that's a researcher's nightmare: finding out that a multibillion dollar corporation is doing the same work you are, but on a much much bigger scale, and may not be interested in sharing their knowledge with you.

Reframing the Liskov Substitution Principle through the Lens of Testing

Who understands the LSP? Nobody, not even Liskov! As the authors put it, it's framed in three properties:

• The Signature Rule: Subtype methods must be compatible with the signatures of corresponding supertype methods.
• The Methods Rule: Calls to the subtype’s methods must behave like calls to the supertype’s methods.
• The Properties Rule: The subtype’s methods must preserve all properties provable about supertype objects.

Students have trouble understanding this, often get details wrong, and don't build a mental model for why LSP is actually important. In particular, students would often switch up whether they were supposed to weaken preconditions and strengthen postconditions, or vice versa. The authors started teaching LSP in a new way, by framing it as "the subtype passes all of the black-box tests by the supertype". They found that students learned LSP more thoroughly this way and hit fewer of the pitfalls they normally did.

I like this a lot and was playing with a similar idea a while back, seeing if you can define LSP as "subtype methods are commutative over lifting to supertype".¹ Watching this talk made me want to explore that more thoroughly, might turn it into an essay if I get anywhere.

After the talk I asked the question "how do you deal with thinking they broke LSP but really wrote a non-blackbox test". According to them, they were able to turn it around and use the LSP to teach the difference between blackbox and whitebox testing! That's a really cool use and one of the reasons I love having multiple ways to understand something. You can use the different explanations to do different things.

Programming and Reasoning with Partial Observability

"Partial observability" meaning there is global state, but we only have partial information on it. In this motivating example, the height of a UAV. While there's an objective "true" height, the UAV measures it with an altometer that adds uncertainty bars. The altometer could read 500 meters while the true height is 450 or 550 meters. The authors want to make programs robust to this uncertainty.

Their approach is "Belief Programming": an approach + language + Hoare logic all based on adding a belief modality to their logic.² Variables can be fixed or nondeterministic:

x = choose(1 <= . && . <= 10);
y = choose(x - 2 <= . && . <= x + 2);

That snippet would say that x is some value between 1 and 10 and y is within two steps of x. There's approximately 50ish configurations of x and y the program has as possibilities. Then □(x + y < 10) is the statement "in all possible configurations, x + y < 10", which is false. ◇(x + y < 10) is "in at least one possible configuration, x + y < 10", which is true.

One thing I haven't been before is that the modes exist on the language level. There's a construct called infer that branches on modes, so you can write infer □P {Q} else {R}, which is pretty cool.

The authors were applying this all to autonomous systems like drones and robots, but I wonder if there's also an application to business modeling. Consider a set of tasks and costs. We have only partial information on what the total project would cost, because on the costs we've already paid, and we're trying to predict if we'll be over or under budget. Being able to say "it's now possible we are over budget" seems like a useful thing.

Pomsets with Preconditions: A Simple Model of Relaxed Memory

I didn't understand very much of this talk, but I really liked how they copresented it. Normally talks with two presenters just have them speak in sequence, one person does the first half and someone else does the second. The authors here instead framed it as a challenge-response between the two, where one person posed the problems and the other person tried to answer them. It's the first time I've seen someone really play with the format in that way.

Then again I also suspect that I'd have had an easier time following it if they went with a more conventional talk.

Demystifying Dependence

What does it mean for module A to depend on module B? Authors presented a bunch of problem cases that mess with our intuition of "dependence", like "does A depend on B if module B can crash the entire program?" They conclude that "dependence" is too ambiguous and we often mean different, contradictory things by it. We have to be specific about what kind of dependency we mean and over what properties we "depend". To help formalize this they argue that dependency is isomorphic to "the domain of causality", as in the philosophical topic.

I'm not sure how convinced I am by this; it seems like they were trying to handle several different deep ideas that weren't "obviously connected". Maybe the paper does more work to unify them all, I haven't read it yet.

To model changing a system they introduce the idea of super-specifications, the set of all permissible modifications to a spec. So a superproperty then would be a property that relates program variations, like "this modification does not make us use any new depreciated APIs." As you all know, I'm a sucker for exotic properties, and now the hunt is on to find a meaningful probabilistic superhyperliveness property.

How Statically-Typed Functional Programmers Write Code

How do people in statically-typed languages actually use the type checker in their day to day work? The authors used a framework called grounded theory, where they look at lots of data, construct a theory that's compatible with the data, and then look at more data to find nuances. In this case, the "lots of data" was 15 programming live sessions and 15 recorded streams.

Lots of goodies in their observations. People use compiler as an "automatic todo list", people intentionally typecheck code they know will not compile, people used a mix of "hierarchical" and "opportunistic" design patterns. I think they also mentioned that people who tried to get all the types right up-front had a more frustrating time than people who iterated on the types, but that's not in my notes and I might have just dreamed it up or something.

Probably the high point talk for me. I think the "grounded theory" framework would be useful for some of my own work and want to investigate it more. Also the main author was a fellow UChicago alum. That place is really hardcore about interdisciplinary education.

Software Architektur Stream

I was on Software Architektur to chat empirical software engineering with Laurent Bossavit and Eberhard Wolff. You can catch the recording here!

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.