Re:Kind: A Modern Proof Language
by LangMakers on Wednesday August 11, 2021 @11:24AM
(#28143119)
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.
[ Parent
| on HN ]
Do you have a plan for cross-consistency checking? Like, for example, Lean was proven consistent by Coq.
Re:Kind: A Modern Proof Language
by Blaisorblade0 on Thursday August 12, 2021 @04:40PM
(#28161151)
Do 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-le..., which was just hard, but it does not prove Lean consistent, it only lets Coq process the Lean stdlib.