Approach

Themes

The goal of Mnemosyne is to automate software development, meaning the writing of code, tests, and types. We interpret tests broadly and any existential program requirement and types broadly as any universal program requirement including simple and refined types, assertions, and logical constraints. As the lion's share of the work on a typical project is adaptation to new requirements and bug-reports this is also the focus of Mnemosyne. The following themes will guide our work on this project.

Familiar.

Existing software development tools including IDEs, programming languages and compilers, test infrastructure, static analyzers, linters, and documentation generators representing decades of advancement in the practice of software engineering are to be extended not replaced. Mnemosyne works directly with existing languages tools and techniques integrating into this ecosystem.

Holistic.

Software developers spend time writing tests, types, and documentation as well as code. For adaptation the descriptions of the intent of the software are often more important than the concrete implementation of the software. Mnemosyne works to synthesize all aspects of a software project—not just code.

Interactive and Transparent.

Most existing synthesis techniques tend to exhibit "all-or-nothing" behavior: they either successfully synthesize a program or fail completely. As a result, code synthesis tools often seem opaque and brittle to users. Successful synthesis-aided software development requires transparency, exposing partial results and incremental refinements to the user. This transparency also provides graceful degradation by enabling the user to step in when full automation is not feasible. In particular we expect that the user will largely handle higher-level structural decomposition and Mnemosyne will help by propagating tests and types down this decomposition and by synthesizing code towards the program leaves.

Innovations

We hope to accomplish these goals—achieving an unprecedented practical application of program synthesis—through the following mechanisms and phenomena.

Hierarchical problem decomposition and incremental refinement.

Mnemosyne will support interactive, incremental synthesis in which the top-level goal is refined into increasingly more concrete sub-problems through continual interaction between the software designer and automated synthesis tools. At each step in the refinement process, the user can either (i) refine the problem specification or software design, (ii) prompt Mnemosyne to automatically synthesize code or (iii) infer additional specifications of sub-problems in the form of tests, types, or documentation. This hierarchical decomposition will enable development of large-scale systems by allowing developers to control the problem's decomposition into modules, without requiring the developer to prematurely commit to low-level implementation choices.

Retention of alternate implementations.

While Mnemosyne will be useful for designing and implementing new software, it will particularly shine for easy and efficient software adaptation. Mnemosyne-enabled software development proceeds in rounds of interactive refinement steps involving both the developer and automated tools, Mnemosyne can leverage this rich refinement history when performing adaptation. Specifically, Mnemosyne will maintain both probability distributions over refinements and populations of diverse concrete implementations. These saved distributions and populations will jump-start subsequent probabilistic and SBSE techniques.

Rich multi-modal intent specifications.

Mnemosyne will allow users to communicate their requirements and preferences using multiple artifact modalities, including test, examples, types, logical constraints, high-level code structure, and natural language. Because different modalities are more convenient for expressing different types of intent users may communicate their intent using the optimal mechanism for the problem at hand. The synthesis and adaptation engines underlying Mnemosyne will leverage these synergistic modalities when performing synthesis.

Mutually reinforcing synthesis modalities.

Mnemosyne's Muses will synthesize mutually reinforcing modalities of program specification and implementation. For example, a type-inference technique will yielding richer type information which may in turn enable a test-generation technique to generate more suitable inputs, which may in turn enable a program-synthesis technique to generate code. In this way the products of Muses will enable other Muses in a virtuous cycle.

Combined probabilistic and logical synthesis.

Mnemosyne will leverage a combination of logical and probabilistic techniques to make correct and efficient code synthesis practical. While logical reasoning is needed to ensure satisfaction of semantic requirements, purely logical reasoning (e.g., based on SMT solvers) is unlikely to scale to real-world software development. Mnemosyne will refine partially realized specifications using code refinements selected from a learned probability distribution of refinements. Besides making synthesis more efficient, probabilistic techniques will also allow Mnemosyne to leverage the latent domain knowledge embedded in existing code by automatically learning prior probability distributions.

Combined probabilistic and SBSE adaptation.

To support efficient adaptation to changing requirements, Mnemosyne will use combined probabilistic and search-based techniques. SBSE techniques have been shown to be applicable to real-world software and are entering real-world use for restricted development tasks. Diversity in software systems is able to jump-start SBSE processes (this same dynamic is familiar from biological systems). By pairing probabilistic refinement and diverse populations—re-weighting probability distributions against concrete population members and evolving populations to fit modified distributions—Mnemosyne will remain poised to quickly and effectively adapt existing implementations to new requirements.

System Architecture

See Architecture for an overview of the architecture of the Mnemosyne system.