This post marks the beginning of a new blog. I’ve been putting off a re-design and re-hosting of this website for the past two years or so, and finally got my hands on it last week.

Introduction

In early 2017, Sumit Gulwani, Rishabh Singh, and I wrote a survey on Program Synthesis. Its goal was to provide a comprehensive overview of the state of the field at the time and to serve as an introduction for newcomers. While complete at the time, the survey got surprisingly outdated in the mere two years. Nowadays, every time someone asks me for an introduction to program synthesis, I point them to this survey but also add 10-20 other links that have recently pushed state of the art. On one hand, this is great: program synthesis is expanding rapidly (ICLR’18 alone had 14 papers on the subject!). On the other hand, I’m getting tired of compiling and annotating these lists of recent links every time 🙂 Ergo, this post — a high-level overview of the recent ideas and representative papers in program synthesis as of mid-2018.

(I overheard this at UW, from a graduate student who told me he doesn’t know the original author of this mnemonic either. Please do not attribute it to either of us 😛).

In PL and formal logic, there exists a common notation, which I personally consider the worst possible notation choice of all times. Let’s say you have an expression $E$, in which you want to replace every occurrence of a variable $x$ (or any other fixed subexpression, for that matter) with another variable $y$ (again, or any other expression). This operation is called substitution ¹. In formal logic, $\lambda$-calculus, etc. there exists a bewildering soup of notations representing this simple transformation:

• $E[x \to y]$ (“$x$ is transformed into $y$”)
• $E[x \gets y]$ (“$x$ is replaced with $y$”)
• $E[x := y]$ (“assign $y$ to every occurrence of $x$)
• $E[y/x]$ (WTF?)

The first two (and their mirrored alternatives) are confusing on its own – you never know which substitution direction the arrow represents (is it “replace $x$ with $y$” or “replace $y$ with $x$”?). But the last one is notoriously ridiculous in that regard. It is too symmetric. How am I supposed to remember which variable substitutes the other one if the only thing denoting this relationship is a meaningless slash character in between? Some say this notation is the easiest to typeset – which is not true, because the third notation also doesn’t use any characters beyond standard ASCII, and it is unambiguous. Anyway, I usually tried to avoid the slash notation as much as possible whenever I could.

However, now I know a beautiful mnemonic, which breaks the “almost-symmetrical” relationship between $x$ and $y$:

“Think of it as $y$ falling over and squishing the $x$.”

Formerly, when someone asked me “How to make my C# program faster?”, my go-to advice was:

1. Improve your computational complexity.
2. Switch to a native language.

Of these suggestions, step #1 should take care of performance in most situations, if done properly. However, sometimes it is not enough. For example, you are writing a user-facing real-time performance-critical application, such as the C# compiler, and you need to look not only at the average performance, but at the 99^th percentile. This is where step #2 used to take over… but not anymore. Currently, my go-to advice looks like this: