A lighweight proof language. Whitepaper.

Formality-Core has multiple reference implementations. Currently, the easiest to install uses JavaScript. First, install npm in your system. Then, on the command line, type: npm -g formality-core. If all goes well, the language should be accessible via the fmc command.

To use it, save a .fmc file. For example, save he file below as main.fmc:

main : <A: Type> -> A -> A
  <A> (x) x

And type fmc main. This should output:

Type-checking main.fmc:
main : <A: Type> -> A -> A

All terms check.

Evaluating `main`:
(x) x

You can also compile .fmc files to JavaScript with fmcjs main, or to Haskell with fmchs main. You can run a script with fmcio main. In this case, main must have an IO type.

Since Formality-Core is so simple, it doesn't come with built-in functions you would expect, and it doesn't have a standard library. But you're welcome to clone the Moonad repository, where we're building several common data structures and algorithms, and contribute!