created_at2022-03-17 17:52:14.417667
updated_at2023-05-11 11:58:57.560218
descriptionA pure functional functional language that uses the HVM.
Sofia Rodrigues (algebraic-sofia)




Kind2 is a functional programming language and proof assistant.

It is a complete rewrite of Kind1, based on HVM, a lazy, non-garbage-collected and massively parallel virtual machine. In our benchmarks, its type-checker outperforms every alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2 unleashes the inherent parallelism of the Lambda Calculus to become the ultimate programming language of the next century.

Welcome to the inevitable parallel, functional future of computers!


Pure functions are defined via equations, as in Haskell:

// Applies a function to every element of a list
map <a> <b> (list: List a) (f: a -> b) : List b
map a b Nil              f = Nil
map a b (Cons head tail) f = Cons (f head) (map tail f)

Side-effective programs are written via monads, resembling Rust and TypeScript:

// Prints the double of every number up to a limit
Main : IO (Result () String) {
  ask limit = IO.prompt "Enter limit:"
  for x in (List.range limit) {
    IO.print "{} * 2 = {}" x (Nat.double x)
  return Ok ()

Theorems can be proved inductively, as in Agda and Idris:

// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
black_friday_theorem     = Equal.refl
black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)

For more examples, check the Kindex.


First, install Rust first, then enter:

cargo +nightly install kind2


New versions probably are not in cargo, so you can install the current version of kind2 by following these instructions:

  1. Install Rust Nightly Toolchain
  2. Clone the repository
  3. cargo install --path crates/kind-cli --force

Then, use any of the commands below:

Command Usage Note
Check kind2 check file.kind2 Checks all definitions.
Eval kind2 eval file.kind2 Runs using the type-checker's evaluator.
Run kind2 run file.kind2 Runs using HVM's evaluator, on Rust-mode.
To-HVM kind2 to-hvm file.kind2 Generates a .hvm file. Can then be compiled to C.
To-KDL kind2 to-kdl file.kind2 Generates a .kdl file. Can then be deployed to Kindelia.

Executables can be generated via HVM:

kind2 to-hvm file.kind2
hvm compile file.hvm
clang -O2 file.c -o file

Commit count: 613

cargo fmt