65 releases
0.3.10  May 11, 2023 

0.3.8  Mar 3, 2023 
0.2.79  Oct 1, 2022 
0.2.32  Jul 27, 2022 
0.1.0  Mar 17, 2022 
#1 in #functionalprogramming
214 downloads per month
17KB
319 lines
Kind2
Kind2 is a functional programming language and proof assistant.
It is a complete rewrite of Kind1, based on HVM, a lazy, nongarbagecollected and massively parallel virtual machine. In our benchmarks, its typechecker 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!
Examples
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)
Sideeffective 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 Nat.zero = Equal.refl
black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)
For more examples, check the Kindex.
Usage
First, install Rust first, then enter:
cargo +nightly install kind2
Warning:
New versions probably are not in cargo
, so you can install the current version of kind2 by following these instructions:
 Install Rust Nightly Toolchain
 Clone the repository
cargo install path crates/kindcli 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 typechecker's evaluator. 
Run  kind2 run file.kind2 
Runs using HVM's evaluator, on Rustmode. 
ToHVM  kind2 tohvm file.kind2 
Generates a .hvm file. Can then be compiled to C. 
ToKDL  kind2 tokdl file.kind2 
Generates a .kdl file. Can then be deployed to Kindelia. 
Executables can be generated via HVM:
kind2 tohvm file.kind2
hvm compile file.hvm
clang O2 file.c o file
./file

If you need support related to Kind, email support.kind@kindelia.org

For Feedbacks, email kind@kindelia.org

To ask questions and join our community, check our Discord Server.
Dependencies
~17–24MB
~389K SLoC