Skip to content
(MIRROR) Moonad Accomplishments, Status, and Goals
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

Moonad Roadmap


Main Accomplishments:

  • Designed the first version of Formality with the aim of developing an efficient proof language for smart-contracts and applications. It included native datatypes and a prototypal interaction-net compiler.

  • Designed Symmetric Interaction Calculus, a parallel model of computation with applications to efficient, optimal and parallel evaluation of functional programs.

  • Explored it and wrote a blog post detailing our insights.


Q1 Accomplishments

Q2 Accomplishments

  • Developed Elementary-Affine-Core (EA-TT), the untyped version of EA-TT.

  • Restructured Formality (the typed proof language) into many sub-projects:

    • Formality-Core (FM-TT): Formality's untyped core, which extends EA-Core with numbers.

    • Formality-Net (FM-Net): Formality's interaction-net, an efficient compile target which extends EA-Net with numbers.

    • Formality-Type-Theory (FM-TT): Formality's underlying type theory, which extends EA-TT with numbers (ongoing).

  • Wrote several FM-Core libraries, including:

    • In-place array library, thanks to linear types!

    • Lists, numbers, tuples and other core FP libs.

    • Ongoing implementation of FM-Core within itself, which will be the base of Formality-Lang.

    • Keccak!

    • A toy game as a demo of its power (and of non-Turing-complete languages!).

  • Finished the EA-Net->EVM compiler. Still needs optimizations. FM-Net next.

  • A prototypal C-backend for FM-Net. (Soon we'll have C++/LLVM experts optimizing it!)

  • Wrote a Github Wiki for Formality-Core.

Current Status (updated: June 22, 2019)

Right now, we're focusing in graduating from the EF and creating our own company. The team size is expected to grow from 4 to about 10 people. Our mission will be to develop Formality as an efficient, user-friendly proof language suitable to write smart-contracts, graphical applications, servers and so on.


Why is Formality important to Ethereum?

Proof languages merge mathematics and programming in a single language. They are secure. Ethereum needs security. We don't have efficient proof languages. Ethereum needs efficienty. Formality is a efficient and Formality is proof language. Thus Ethereum needs Formality. QED. (TODO: formal proof)

You can’t perform that action at this time.