Kind2

This is a prototype of Kind-Lang's successor. It does NOT include all of the Kind1 features yet, and won't for a while, but it already has the building blocks to create programs and proofs. It is designed to be maximally compatible with HVM. New features were added with that goal in mind.

Usage

1. Install it

First, install Rust. Then, type:

cargo install kind2

2. Create a Kind2 file

Kind2 files look like HVM. Save the file below as main.hvm:

// Booleans
Bool : Type
  True  : Bool
  False : Bool

// Negates a boolean
(Bool.Not b:Bool) : Bool
  (Bool.Not True)  = False
  (Bool.Not False) = True

// Double Negation Theorem
(Bool.DNT b:Bool) : (Bool.Not (Bool.Not b)) == b
  (Bool.DNT True)  = refl True
  (Bool.DNT False) = refl False

3. Type-check it

kind2 check main.kind2

4. Compile it to HVM

... TODO ...