FormCore.js port to Dart.
So far only the parser and typechecker have been
ported i.e. the FormCore.js file in the original
repo.
(Original readme from https://github.com/moonad/FormCoreJS)
FormCoreJS
A pure JavaScript, dependencyfree, 700LOC implementation of FormCore, a minimal proof language featuring inductive reasoning. It is the kernel of Kind. It compiles to ultrafast JavaScript and Haskell. Other backends coming soon.
Usage
Install with npm i g formcorejs
. Type fmc h
to see the available commands.

fmc file.fmc
: checks all types infile.fmc

fmc file.fmc js main
: compilesmain
onfile.fmc
to JavaScript
As a library:
var {fmc} = require("formcorejs");
fmc.report(`
id : @(A: *) @(x: A) A = #A #x x;
`);
What is FormCore?
FormCore is a minimal pure functional language based on self dependent types.
It is, essentially, the simplest language capable of theorem proving via
inductive reasoning. Its syntax is simple:
ctr  syntax  description 

all  @self(name: xtyp) rtyp 
function type 
all  %self(name: xtyp) rtyp 
like all, erased before compile 
lam  #var body 
pure, curried, anonymous, function 
app  (func argm) 
applies a lam to an argument 
let  !x = expr; body 
local definition 
def  $x = expr; body 
like let, erased before check/compile 
ann  {term : type} 
inline type annotation 
nat  +decimal 
natural number, unrolls to lambdas 
chr  'x' 
UTF16 character, unrolls to lambdas 
str  "content" 
UTF16 string, unrolls to lambdas 
It has two main uses:
A minimal, auditable proof kernel
Proof assistants are used to verify software correctness, but who verifies the
verifier? With FormCore, proofs in complex languages like Kind
can be compiled to a minimal core and checked again, protecting against bugs on
the proof language itself. As for FormCore itself, since it is very small, it
can be audited manually by humans, ending the loop.
An intermediate format for functional compilation
FormCore can be used as an common intermediate format which other functional
languages can target, in order to be transpiled to other languages. FormCore’s
purity and rich type information allows one to recover efficient programs from
it. Right now, we use FormCore to compile Kind
to JavaScript, but other source and target languages could be involved.
The JavaScript Compiler
This implementation includes a highquality compiler from FormCore to
JavaScript. That compiler uses type information to convert highly functional
code into efficient JavaScript. For example, the compiler will convert these
λencodings to native representations:
Kind  JavaScript 

Unit  Number 
Bool  Bool 
Nat  BigInt 
U8  Number 
U16  Number 
U32  Number 
I32  Number 
U64  BigInt 
String  String 
Bits  String 
Moreover, it will also convert any suitable userdefined selfencoded datatype
to trees of native objects, using switch
to patternmatch. It will also swap
known functions like Nat.mul
to native *
, String.concat
to native +
and
so on. It also performs tailcall optimization and inlines certain functions,
including converting List.for
to inline loops, for example. The generated JS
should be as fast as handwritten code in most cases.
Example
The program uses self dependent datatypes to implement booleans, propositional
equality, the boolean negation function, and proves that double negation is the
identity (∀ (b: Bool) > not(not(b)) == b
):
Bool : * =
%self(P: @(self: Bool) *)
@(true: (P true))
@(false: (P false))
(P self);
true : Bool =
#P #t #f t;
false : Bool =
#P #t #f f;
not : @(x: Bool) Bool =
#x (((x #self Bool) false) true);
Equal : @(A: *) @(a: A) @(b: A) * =
#A #a #b
%self(P: @(b: A) @(self: (((Equal A) a) b)) *)
@(refl: ((P a) ((refl A) a)))
((P b) self);
refl : %(A: *) %(a: A) (((Equal A) a) a) =
#A #x #P #refl refl;
double_negation_theorem : @(b: Bool) (((Equal Bool) (not (not b))) b) =
#b (((b #self (((Equal Bool) (not (not self))) self))
((refl Bool) true))
((refl Bool) false));
main : Bool =
(not false);
It is equivalent to this Kind
snippet:
// The boolean type
type Bool {
true,
false,
}
// Propositional equality
type Equal <A: Type> (a: A) ~ (b: A) {
refl ~ (b: a)
}
// Boolean negation
not(b: Bool): Bool
case b {
true: false,
false: true,
}
// Proof that double negation is identity
theorem(b: Bool): Equal(Bool, not(not(b)), b)
case b {
true: refl
false: refl
}!
The GitHub Link: