Mnemo

(Apollo dancing with the Muses)
Mnemosyne provides automated software development collaborators or "muses."

Mnemosyne

Mnemosyne: Titan goddess of memory and remembrance, inventor of language, mother of the muses.

Mnemosyne is your automated software development assistant. It integrates with your IDE and works with you suggesting code, types, and tests as you work; and continually checking the consistency of your documentation, types, tests, and implementation—whether that means running test suites or type checkers, or using ML techniques to ensure your documentation matches your implementation. Mnemosyne applies statistical machine learning, formal methods, and Search Based Software Engineering (SBSE) to enable developers to write higher quality, higher assurance, and more standards compliant code more quickly. Mnemosyne transcends CI/CD by making live substantive contributions to the software development process as the developer works. Mnemosyne speaks LSP, meaning it integrates seamlessly with most popular text editors and IDEs. Mnemosyne is extensible, easily collaborating with varied program synthesis modules or "Muses."

QuickStart

See Usage for detailed usage information.

  1. Download and run the Argot Server docker image.

    docker run --rm -p 10003:10003 mnemo/argot-server
  2. Open a C, C++, Python, JavaScript, or Common Lisp file and connect your editor or IDE to the server.

    From Visual Studio Code:

    1. Install the Mnemosyne VS Code extension. (How to install a .vsix file.)
    2. Open Command Palette (Control+Shift+P) and connect to the Argot Server with Mnemosyne: Connect to Argot Server.
    3. Implicitly invoke Mnemosyne by selecting part of the file.

    From Emacs:

    1. Install Eglot M-x package-install-package eglot RET.
    2. Connect to the Argot Server with C-u M-x eglot using localhost:10003 for the host and port.
    3. Explicitly invoke Mnemosyne on an active region with M-x eglot-code-actions.

    From Vim:

    1. Install LanguageClient-neovim using Plug.
    2. Configure the language client to use Argot Server:
      use let g:LanguageClient_serverCommands = {
      \ 'python': ['tcp://localhost:10003'],
      \ 'cpp': ['tcp://localhost:10003'], etc... }
    3. Explicitly invoke Mnemosyne on the visual selection with :call LanguageClient#textDocument_visualCodeAction().

Architecture

See System Architecture for detailed design information.

Mnemosyne extends Microsoft's LSP protocol for IDE integration to support decorating program subtrees with tests, types, and prose. We call this extension "Argot LSP," or “Argot” for short.

Argot

Inside Mnemosyne Argot allows automated techniques of program test generation, program analysis, type and invariant inference, and program synthesis and refactoring (we call these modules "Muses") to communicate with each other as well as with the developer's IDE.

Mnemosyne Architecture

The result is a collaborative environment centered around the developer where suggestions for new tests, types, and code edits are continually made against the software code base. The result is improved developer productivity and software quality.

Muses

See Muses for a complete list of the Modules or Muses currently implemented and under development for Mnemosyne with demo videos. Some of these include:

NameDescriptionVideo
Argument Predictor probabilistic completion of callsite arguments
DIG trace-based invariant generation technique
Galois Autocomplete machine learning based code completion
GenPatcher automated program repair
Herbie improve floating-point code stability and accuracy
Hypothesis Tests type-driven automated testing
Snippet Mining example API usage snippets
SSR AST-level software search and replace
Trinity extensible systhesis framework for data science

Note: Due to an open bug in GitLab's pages feature (gitlab-pages#504, forum/44691) videos don't render in Safari.

Goals and Approach

See About for general information about the project and Approach for our top-level themes and approaches to human/computer collaboration.

The Mnemosyne project was started by GrammaTech in collaboration with leading program synthesis researchers: Swarat Chaudhuri and Işıl Dillig from UT Austin, and Armando Solar-Lezama from MIT.

Research in program synthesis and automated software engineering has leapt forward in recent years thanks to advances in underlying machine learning and constraint solving technologies. We hope to bridge research and practice by connecting research technologies to modern programming languages and IDEs. To ensure practical utility we focus on the following themes:

  • Transparency: All results of muses are displayed to the developer using familiar tests, types, and code edits.
  • Interactivity: The developer's activities guide muses and curate their results. Smaller more focused developer interactions are prioritized over coarse-grained large-scale synthesis.
  • Incrementality: Intermediate results are communicated back to the developer and the software project. Synthesis techniques that proceed function by function are prioritized when scalability is in question.

Copyright (C) 2021 GrammaTech, Inc.

This material is based upon work supported by the US Air Force, AFRL/RIKE and DARPA under Contract No. FA8750-20-C-0208. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the US Air Force, AFRL/RIKE or DARPA.