[skybrian]

The plan for Kind itself seems to be to allow possibly unsound expressions (for example that don’t terminate), but to have consistency checkers. See:

https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...