Pure & spatial synthesis

To allow for synthesis from richer specifications: Mutually recursively use pure synthesis to restrict spatial synthesis and visa-versa?

Further generalize fold?

It seems like folds are only between data structures of “known” layout. Can this be generalized, maybe using the predicate lambdas?

Can we more easily specify certain kinds of conversions between data structures using such a fold?

Syntactic transformations

What is the relationship between staging (such as in Frank Pfenning’s work and Ningning Xie’s work) and the SuSLik syntactic transformations, if any? Could this prior work be useful for guiding us in how to implement and specify/verify these transformations?

See Pfenning's modal logic-based work on staging, for instance. Pfenning gives a sort of survey talk about this here.

Should we try to ensure the internal syntactic transformations we're adding to SuSLik are type-safe (particularly with regard to capture-avoidance and being well-scoped), similar to how GHC Core (an intermediate language used by the Haskell compiler GHC) is type checked during the compilation process? Maybe a modal type system could help here.

"Complexity annotations"

Would it be helpful/possible to have “complexity annotations” for SuSLik to restrict the search space to only programs which have a certain asymptotic complexity (or faster)? See, for instance, ReSyn for one approach to how these annotations might be specified (here and here)

Rust backend

Rust backend for SuSLik

How does synthetic separation logic interact with Rust’s type system and borrow checker?

Could we, in effect, write “functional” specifications for Rust code that could then get automatically synthesized?

Maybe we can use such a system to implement a concrete, relatively practical example.

A different, possibly useful, perspective on mathematical relations

Again, this is a potential place where modal logic could be used. Since we are looking at a sort of “relational” perspective on SuSLik, would modal logic be useful here? Modal logic essentially enables a certain kind of reasoning about "relational structures" (a relational structure is any set with relations defined on it). TODO: Find a brief reference to put here outlining the basics of modal logic and its connection to relational structures to illustrate this

Connection to database theory?

Along the lines of the above mention of modal logic, is there a connection between the proposed SuSLik join operation (and related constructs) and database theory and relational algebra?

Non-regular datatypes

Can non-regular datatypes, such as finger trees and FunLists, be expressed in SuSLik?

Enriching SuSLik's constraint solving for the pure parts

Consider constraint solving with propagators (also see these slides and this Haskell package) that are enriched with pre/post conditions as a "preprocessing step" before SuSLik tries to use its solver. Is this possible?

For example, consider solving 3*y == 2*x for y given the “precondition” that exists z, x == 3*z. In this case, we can safely divide x by 3 and be guaranteed that the result will be an integer.

Maybe this can be used to extend SuSLik’s pure solving capabilities

“Pure inductive predicates”

Composability of predicates appears to be somewhat of an issue. To help with this, we could consider adding "pure inductive predicates" to SuSLik.

Similar to inductive predicates, but they have no spatial part. This could potentially be used to enable a simple, but possibly useful composition mechanism.

These could be implemented using a syntactic transformation. When used as a (standard) inductive predicate, it would generate a standard inductive predicate without a spatial part. When it is used in a composition, composes the pure parts.

This way, we can have multiple predicates (in this case, "pure inductive predicates") which conceptually apply to the same memory location without violating the rules of separating conjunction. This is accomplished by the above mentioned syntactic transformation combining two "pure inductive predicates" into a single one.

Also, there could be a mechanism for "adding" a spatial part to a pure predicate, allowing separation of these two things which could be useful.

Another form this could take: We could automatically generate "pure inductive predicates" for any existing predicate by just "forgetting" the spatial part. This might help reduce code duplication when working with pure inductive predicates.