-
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.
-
Implemented and explored Cedille-Core, a minimal proof language designed by Aaron Stump.
-
Based on it, developed a 800 LOC type-theory compatible with optimal reductions, previously called Formality, which we now call Elementary Affine Type Theory (EA-TT).
-
Based on Symmetric Interaction Combinators, developed Elementary Affine Net (EA-Net), an interaction net system and compile target for EA-TT.
-
[Stated and proved several theorems on EA-TT](proofs and libraries), to validate and explore its expressivity.
-
Wrote a blog post introducing it.
-
Started working on the Moonad Operating System, but stopped to focus in developing an efficient proof language.
-
Started a compiler to the EVM.
-
Developed a HTML/JS animation tool for EA-Net.
-
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.
Way too many things to type here now :) Formality is getting mature, nearing a stable 0.1 release, its base libs are growing, everything is great. Check out https://github.com/moonad/formality! Yay. (For any questions, feel free to open an issue here.)