Kind2: a parallel proof & programming language

Kind2 is a general-purpose programming language made from scratch to harness HVM's massive parallelism and computational advantages (no garbage collection, optimal β-reduction). Its type system is a minimal core based on the Calculus of Constructions, making it inherently secure. In short, Kind2 aims to be:

• As friendly as Python

• As efficient as Rust

• As high-level as Haskell

• As parallel as CUDA

• As formal as Lean

And it seeks to accomplish that goal by relying on the solid foundations of Interaction Combinators.

Usage

1. Install Rust and (optionally) Haskell in your system.

2. Clone this repository and install it:

   git clone https://github.com/HigherOrderCO/Kind2
   cargo install --path .
   

3. Type-check a Kind2 definition:

   kind2 check name_here
   

4. Test it with the interpreter:

   kind2 run name
   

5. Compile and run in parallel, powered by HVM!

   kind2 compile name
   ./name
   

Syntax

Kind2's syntax aims to be as friendly as Python's, while still exposing the high-level functional idioms that result in fast, parallel HVM binaries. Function application ((f x y z ...)) follows a Lisp-like style and pattern-matching (match x { ctr: .. }) feels like Haskell; but control-flow is more Python-like. In short, it can be seen as "Haskell inside, Python outside": a friendly syntax on top of a powerful functional core.

Functions:

// The Fibonacci function
fib (n: U60) : U60 =
  switch n {
    0: 0
    1: 1
    _: (+ (fib (- n 1)) (fib (- n 2)))
  }

Datatypes (ADTs):

// Polymorphic Lists
data List T
| cons (head: T) (tail: (List T))
| nil

// Applies a function to all elements of a list
map A B (f: ∀(x: A) B) (xs: (List A)) : (List B) =
  match xs {
    cons:
      let head = (f xs.head)
      let tail = (map _ _ f xs.tail)
      (cons _ head tail)
    nil:
      []
  }

Theorems and Proofs:

use Nat.{succ,zero,half,double}

// Proof that `∀n. n*2/2 = n`
bft (n: Nat) : {(half (double n)) = n} =
  match n {
    succ: (Equal.apply _ _ succ _ _ (bft n.pred))
    zero: {=}
  }

More Examples:

There are countless examples on the Book/ directory. Check it!