This is an interesting idea but is there any description of the soundness of this approach? Any functionality capable of subsuming not just inductive types but higher-inductive types is going to be very subtle. I looked around on the repository but I can't find any formal description of the language or type theory, which is worrying for a proof tool.

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#...

There's a paper on the soundness of self types: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...

I'm not in the field. For anyone else curious about relationship to things like TLA+ (https://en.wikipedia.org/wiki/TLA%2B) - the discussion at https://news.ycombinator.com/item?id=15583377 was great.

So, on one hand I totally think there’s some really cool expressivity in these “everything is a lambda” language experiments.

On the other hand, it makes efficient runtime (runtime is a tricky word here ;) ) representation of data types a bit more opaque! Or at the very least I’ve seen little work that attacks that problem.

That said, perhaps all the optimization tricks developed for self and small talk etc are the answer here?