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 fm command.
To use it, save a .fm file. For example, save the file below as main.fm:
main : <A: Type> -> A -> A
<A> (x) x
And type fm main. This should output:
Type-checking main.fm:
main : <A: Type> -> A -> A
All terms check.
Evaluating `main`:
(x) x
You can also compile .fm files to JavaScript. First, run fm to generate a
.fmc. Then, run fmcjs main. You can also compile 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!