Our goal is, in essence, to synthesize C-like code from a Haskell-like specification.

Comparing this to the way a traditional Haskell compiler works, there are a few advantages to this. The first two advantages are nearly complementary.

1. Higher-level specification

In Haskell, "specifications" (Haskell code) uniquely specifies the generated object code (assuming the collection of REWRITE rules involved, if any, is confluent). While this can be useful, it also puts limits on how high-level the "specification" can be.

We may not care about the specific behavior of one part of the program, so long as it satisfies a certain specification. For instance, we might not care how a list gets sorted, so long as it gets sorted.

Furthermore, we have access to all of SuSLik's existing specification capabilities, particularly its ability to describe transformations between data structures. For example, synthesizing a function that flattens a binary tree into a linked list from a simple specification.

2. Memory behavior

In some ways, this is almost the opposite of the first point. In Haskell, we have little control over the low-level memory behavior. This can lead to space leaks, particularly in the presence of laziness which can make the existence and location of space leaks less intuitive.

Here, however, we have exact control over the behavior of the program w.r.t. the heap. In particular, we have full control over when allocation occurs and when deallocation occurs. This makes it significantly easier to avoid space leaks.

Predictable memory behavior can be especially important in embedded systems and hard real-time applications.

3. In-place algorithms

We can directly give specifications that can only be synthesized through the use of an in-place algorithm. Such algorithms are often more efficient than any non-in-place equivalent.

This is also possible in Haskell, but it is less succinct and somewhat more complex as you must go through (for example) the ST type. Defining and working with data structures that have certain kinds of cyclic structure, such as a doubly-linked list, is also more complex in Haskell.

4. Expanding the expressiveness of SuSLik specifications

In Structuring the Synthesis of Heap-Manipulating Programs by Nadia Polikarpova and Ilya Sergey (2019), the beginning of the Motivation subsection of the Introduction states:

The goal of this work is to advance the state of the art in synthesizing provably correct heap-manipulating programs from declarative functional specifications.

By adding new features, such as the ability to compose specification-level "functions," we extend SuSLik further towards this goal.

We are enriching SuSLik's declarative specification language.