Of the things I'm familiar with that are out there, this looks most familiar to Idris 2. Also, while Lean is primarily used for mathematical proofs, Lean 4 is beefing up its capabilities to be used as a regular programming language as well. Can anyone speak to the differences between this and those?
I am still very new to proof theory. So please take this with a mountain of salt.
At the core all these proof assistants, is a dependent total functional programming language.
Total means all functions must be obviously be terminating.
Dependent means types can dependent on values or more generally you can have quantifiers (sigma and pi).
Both Coq and Lean have variants of a dependent type theory called “Calculus of Inductive Constructions”.
Coq and Lean have tactics which can be thought of an embedded “proof language”. It’s an useful fiction because underneath it is just functions and inductive definitions.
Agda and Idris doesn’t have tactics, so the proofs have to be done through computation (by defining and apply functions and data types)
Lean and Coq differ in how they encode mathematical objects. Lean makes it much easier to make use of classical axioms. (Defining axioms is easy in both Lean and Coq)
From a more practical POV, Coq has the best documentation, books and development tools.
Lean has the WORST development tools of all 4. However has extensive libraries for mathematics. ( It is very painful to use )
Agda and Idris are about the same (set up is a pain otherwise about as good as Haskell development)
Even though Idris is marketed for “practical programming” it doesn’t have partial functions!!
Total means that the function must always return a value. In the presence of coinductive types and corecursive functions, a total function can run forever but must always be producing values when asked. e.g. an infinite stream of prime numbers can be produced by a corecursive, total function. You can use this to embed Turing complete computations in languages like Agda or Coq[1], they just must be declared as such up front. Much like IO must be declared up front in (idiomatic) Haskell. And much like you can unsafePerformIO in Haskell, Idris and Agda have their own escape hatches as the sibling comment mentions.
I have heard multiple authors and speakers (while watching various lectures and in papers) say emphatically that no one wants to deal with coinductiion in a type theory unless they ABSOLUTELY must. I'm not sure I've ever seen a concise explanation of the complications that arise by inserting coinductive types into a type theory, but I'll take it as an article of faith that the issues exist. But, the concept is certainly intriguing. Somehow, in my reading on type theory there has been a lack of exploration of instantiation of coinductive types, hopefully the paper by McBride you linked will give me some references to chase down.
Not all proof assistants are based on dependent type theory. The HOL family is based on simple type theory + a classical axioms: you get choice, excluded middle, extensionality etc. in exchange for a less powerful type system. Maybe not coincidentally, Isabelle/HOL also has arguably the most powerful automation thanks to its ability to call automatic provers, almost all of which are based on non-dependent classical logic.
Other non-dependent type theory systems are Mizar, the B method, TLAps…
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.
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.
