Brief history of Kind?

[ken-okabe]

Hi, I'm pretty new to Kind language and I'd like to know the project outline in a historical aspect.

I've read Formality is the old language and It evolved and became Kind, its successor.

I wonder how the language or project structure has been evolved because I've found the documents for Formality are still very interesting and a good subject to learn stuff; however still I want to use the newer language, Kind so, I want to know the difference between the old Formality and the latest Kind implementations.

What exactly is the difference between Formality and Kind, and what has been the motivation to switch the project and language itself? Thanks!

[algebraic-dev]

Kind uses a simple Calculus of Constructions system instead of Self Types (right now) and compiles to HVM

[lukaszlew]

How are types of data type eliminators decided? The are not in CoC.

[algebraic-dev]

Yeah, I mean It's not a complete CoC at all (as it does not have a Hierarchy of Universes and uses Type-in-Type instead and so we can code some eliminators), I think that Andrej Bauer called it Spartan Type Theory.

[zicklag]

Here's a repo I found on Spartan Type Theory with some good slides and some other resources linked to here.