HigherOrderCO
How the Kind proof assistant works (the implementation)?
So to briefly summarize, here is what I have seen so far:
- THEOREMS.md, which gives some example exercises on how to use the Kind proof assistant.
- FMC_SPECIFICATION.md, and old document it looks like, but super helpful for knowing some of your all thought processes.
- FormCore.js A very small type theory with dependent types in JavaScript.
- The blog and self types intro.
- Examples in Kind.
- Kind implementing itself?
So I have to explore the last one some more, but have explored the rest (though I haven't done the theorem tutorial yet, just browsed through it). I also ordered a copy of TAPL, to learn more about how to implement type theories. Even looking at your FormCore.js and how simple it is, I don't know the reasoning as to why things were done the way they were done. It would be super helpful if you could add some annotations to it or create a blog post about the theory behind it, or if you already have something out there please share the link :). I know it's about dependent types, but why did you include each piece (App, Var, etc.), and how do the algorithms generally work, etc.
I have a sort of foundational question. I have an undergraduate science degree, so took up to calculus in math, learned software engineering and computer science on my own, and am slowly learning math / type theory (I know basically up through basic abstract algebra, not really category theory, proof theory, or much type theory). I don't know how to do proofs, but I gather it is simply about rewriting terms until the left and right sides match (or top and bottom), applying theorems and rules and such. But I don't get it beyond that, it's still a black box mystery to me!
My first exposure to real math and type systems was with Coq and HoTT. I found that while looking for a mathematical system that could be used in code, and I wanted to figure out how to write proofs instead of just unit tests in code, like I've seen you all mention in the docs. I looked through the HoTT codebase, played a little with the proof assistant, tried to apply some "proof tactics", but still felt like it was a black box mystery and it was very unintuitive, and I don't know why things need to be modeled the way they do. Like why do we need to model the natural numbers as a sequence with succ and Peano's axioms and all that? Etc. tons of fog when I look into the proof assistant / automated theorem proving world. But I want to crack the nut!
It totally looks like Kind lang and the community has fully mastered all of this stuff, obviously 🙂. What I wanted to ask was if you could put together a blog post, or just point to the write things or whatnot in this thread, on how to get where you are in terms of knowledge and grasp of the various type theories/systems and proof assistant implementation stuff. What needs to be studied? What were the key roadblocks that you got past that would be of use to know about, and how did you get past them haha basically. That would be the ideal to know at least.
But in terms of practicality, would love to know how the proof assistant works in some technical detail. First, where is the implementation exactly? Second, what does it technically do when it reads your "proof"? And what exactly is a proof in Kind lang? (i.e. what are all those things you are doing in the THEOREMS.md doc?). When you write a proof, what are you writing? (types? functions? something else?). What does the code do which does the proving correct or disproving (meeting the goals), how does that work?
Anyways, probably a long discussion. Was going to reach out on telegram but it doesn't want to work on my phone and I'm too afraid to download external software on my laptop. Looking forward to hearing from you all! Hopefully there is some piece to this you would feel cool with sharing, I know you all have a wealth of knowledge in there to share. So excited to have found kind lang, it looks so cool and is already teaching me a lot.
Hi, I'm also still learning a ton of stuff, but I'm almost finished reading TaPL, and when you read it you'll recognize a ton of terms/concepts that are applied in Kind and similar languages, stem from primary concepts of a type theory and an implementation of it.
I am not at all in the same level of experience as the library's maintainers/contributors, but I think I can aid in just pasting a few links that helped me.
But talking about dependent types, you basically have another "axis" of flexibility that you can use to prove propositions(https://en.wikipedia.org/wiki/Lambda_cube). Also related videos:
- https://www.youtube.com/watch?v=SknxggwRPzU
- https://www.youtube.com/watch?v=U5i2VQj5jPk
There's also the "advanced topics in TaPL" that stems from the "original TaPL" book.
And there's also this Reddit thread that people gave their opinion about reading TaPL, and what to do next: https://www.reddit.com/r/types/comments/5r8sv0/how_well_has_pierces_types_and_programming/
I recommend going through "Software Foundations". It teaches theorem proving in Coq. The learning curve is not too steep if you know a bit of programming. For the implementation of dependent type theories I recommend this repo: https://github.com/AndrasKovacs/elaboration-zoo (though these theories are different from Kind).
