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.
Install requires Rust: cargo +nightly install kind2
https://github.com/Kindelia/Kind
A minimal, efficient and practical programming language that aims to rethink functional programming from the scratch, and make it right. Under the hoods, it is basically Haskell, except without historical mistakes, and with a modern, consistent design. On the surface, it aims to be more practical, and to look more like conventional languages. Kind is statically typed, and its types are so powerful that you can prove mathematical theorems on it.
Last modified 18 May 2025