4 ms·
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 Hask
by LangMakers 5y ago
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.
- klyrs 5y agoDo you have a plan for cross-consistency checking? Like, for example, Lean was proven consistent by Coq.
- Blaisorblade0 5y agoDo you have a link? That might mean a set of different things, ranging from very hard to impossible; strictly speaking, this seems to go against Godel's theorems tho there are standard workarounds. I'm familiar with https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581 https://coq.discourse.group/t/alpha-announcement-coq-is-a-le..., which was just hard, but it does not prove Lean consistent, it only lets Coq process the Lean stdlib.