Comment by LangMakers

Note that Kind is NOT terminating by default. It takes the opposite stand. Expressivity is the default, so you can write recursions and loops freely, as in Haskell or any other conventional language. Consistency is a planned opt-in, which you may use to ask Kind's compiler to check for termination of mathematical proofs specifically.