On: Compilers for the Future

[abeppu]

> I call it program synthesis. In ChatGPT you can get ChatGPT to generate code, so this kind of already exists.

This is cool, but to be clear work on program synthesis predates ChatGPT by _decades_. For a long time the work was searching for a program which met some behavioral specification. Emphasis shifted later towards inductive "programming-by-example" where we synthesize a program based on a small set of inputs and outputs, in part because providing those examples is often easier than thinking through an exact "specification" of what you want.

Some work from the '70s https://dl.acm.org/doi/10.1145/362566.362568 https://dl.acm.org/doi/10.5555/1624626.1624666

Some 21st century work on inductive synthesis https://link.springer.com/chapter/10.1007/978-3-319-21690-4_...

ML + symbolic inductive synthesis: https://arxiv.org/pdf/1809.02840v1.pdf

[samsquire → abeppu]

Thank you for your reply and thank you for links to 3 (!) whitepapers.

What do you think is a good behavioural specification? I have often thought that: given a log (read: a highly accurate trace of what the program did) of a program, the log indicates what the program does and there are relations between the fields in the log and log lines.

If some program generates the same log, with the same input and output, is the behaviour of that program identical?

Now I want to do these things:

* provide example logs, which are desired behaviour and let the computer work out the code to fulfil that example

* combine the behaviours of one or more programs

* convert log into a tree or graph that resembles invocation stack (for functional application synthesis, such as "this log resembles a post order traversal" or "a normal form")

* tweak the behaviour of one program with the behaviour of another program, "use one program as a tool in the other program"

Could we wire up the logs and cause things to the code that generated them? The log is a bidirectional view into the program's operations and code that generated it.

In other words, modify code and behaviour by modifying behaviours directly and rely on causality feeding backwards through a chain of logic.

[abeppu → samsquire]

I think different contexts call for different kinds of specification, but most commonly, I do think "synthesize a _function_ which for inputs x1, x2, ..., xk produces outputs y1, y2, ..., yk respectively", is a pretty good setup provided you then are willing to test it on xk+1 ... xn. The "programming-by-example" research direction aligned nicely with TDD, and functions provide a nice abstraction layer.

I _don't_ think a detailed program trace is the best "specification" in most cases because constructing that log includes making a lot of choices of _how_ the program arrives at its outputs. The full trace for meaningful programs might be quite large, and onerous to specify (or you'd just produce one from an already-working program, in which case what's the point?).

For me, the benefit of synthesis should be that the programmer can describe what should be done, rather than how. However, this can quickly lead to a complex "specification language" which can be just as burdensome to write in as the desired target language, which is why examples are appealing. But perhaps some combination, where we provide some examples and also some formally specified restrictions ("the `get_work_history` method returns `jobs: List[Jobs]` such that `map(_.start_date, jobs)` is non-decreasing according to the default comparator on Dates ...") is best, since examples will generally underspecify the program.

Update: the 'different contexts' I think is mostly that sometimes, some specific attributes of 'how' the synthesized program accomplishes its goals do matter -- e.g. you may want to synthesize some mathematical optimization code which really ought to use the GPU, and that isn't indicated in just input/output examples, or you may want to ensure that part of an embedded system uses constant memory and returns after a constant number of steps.