Coq is based on OCaml and similar to it but actually forms its own completely independent language. Others in the same vein are Agda, Idris, Epigram, Isabelle. Each one shares more similarities with the others than with their "host" language (if one exists) of which they're usually syntactic cousins.
That said, each of them is far more similar to OCaml/Haskell than say, C.
They are all based to some degree or another on Martin Löf's Intuitionistic Type Theory which is a wonderful unification of mathematical logic and straightforward functional programming in the same vein as the Curry-Howard Isomorphism.
Generally, much of the forward research is aimed at making the proofs more automatic and easier to use. The problem is wildly intractable by brute force, so much cleverer tricks must be employed. Some of these are quite wonderful and suggest new ways of programming as a dialogue between a human and an intelligent compiler that I really hope become more common in the future, though the industry will be unlikely to drive it. See the literature on Epigram for some talk about this.
There's also an important distinction between proof systems and "dependently typed languages" where proof systems restrict their power greatly so as to ensure the things which are proved in them are mathematically consistent while dependently typed languages which are more "practical" seek only to provide proof-like heuristic support to programming. In the former, you'll likely see a complex way of describing group theory in the language of program types and the program itself is irrelevant because its mere existence is sufficient for logical purposes. In the latter, you'll see a strong synthesis of a program and its internal logic as expressed by its types which ensure that invalid programs are wildly difficult to write as you'll likely have to abuse some crazy flaw in intuitionistic logic in order to do so.
The most canonical example is the fixed-length vector where you can write things like "append takes two vectors and results in one that's the sum of their lengths" and thus track (statically!) that you have no out of bounds errors possible in your program. It's also incredibly useful for getting nice properties like "this vector-of-vectors representation of a matrix is not ragged" confirmed at compile time... something that even an advanced non-dependently typed language like Haskell or OCaml is (mostly) strictly in the domain of runtime checking.
Neither Coq nor Isabelle are based on Martin-Löf Type Theory (in a narrow sense).
Coq is based on a variant of the calculus of construction (with (co)inductive definitions) and Isabelle is an LCF-style prover framework that you can instantiate with various different logics. The most widely used variant is Isabelle/HOL which implements a variant of Church's theory of types. To implement other logics, Isabelle uses intuitionistic second order logic based on lambda calculus, without numbers or recursive data types. Idris has Type:Type, so is unsound as a logic. I'm not sure exactly what Epigram uses, but I assume it's somehow based on Luo's ECC. Only Agda is based on Martin-Löf Type Theory.
Yeah... This is correct as far as I know though a bit out of my complete technical grasp. To my understanding MLTT was a fairly central topic and it helps to distinguish MLTT from just type theory since plain-old-TT might be harder to distinguish as something interesting above `(int *)`.
But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.
Per Martin-Löf was instrumental in extending type theory to dependent types, although the first version of his dependent type theory was impredicative with Type:Type and was shown to be inconsistent by J.-Y. Girard. Subsequent versions of Martin-Löf type theory have been predicative, but other dependent type theories (such as the calculus of constructions) stuck with (more benign forms of) impredicativity.
Thanks for the theorical background. I just had a look at the Curry-Howard Isomorphism article on Wikipedia, and i finally understood what my OCaml teacher muttered once in the classroom 10 years ago :))
The part i didn't get in the equivalence between program and proof, is that a function can be seen as a proof that provided the input parameters are of a given type, the output type is going to be that one. Quite simple in fact, but it only clicked right now :)
That said, each of them is far more similar to OCaml/Haskell than say, C.
They are all based to some degree or another on Martin Löf's Intuitionistic Type Theory which is a wonderful unification of mathematical logic and straightforward functional programming in the same vein as the Curry-Howard Isomorphism.
Generally, much of the forward research is aimed at making the proofs more automatic and easier to use. The problem is wildly intractable by brute force, so much cleverer tricks must be employed. Some of these are quite wonderful and suggest new ways of programming as a dialogue between a human and an intelligent compiler that I really hope become more common in the future, though the industry will be unlikely to drive it. See the literature on Epigram for some talk about this.
There's also an important distinction between proof systems and "dependently typed languages" where proof systems restrict their power greatly so as to ensure the things which are proved in them are mathematically consistent while dependently typed languages which are more "practical" seek only to provide proof-like heuristic support to programming. In the former, you'll likely see a complex way of describing group theory in the language of program types and the program itself is irrelevant because its mere existence is sufficient for logical purposes. In the latter, you'll see a strong synthesis of a program and its internal logic as expressed by its types which ensure that invalid programs are wildly difficult to write as you'll likely have to abuse some crazy flaw in intuitionistic logic in order to do so.
The most canonical example is the fixed-length vector where you can write things like "append takes two vectors and results in one that's the sum of their lengths" and thus track (statically!) that you have no out of bounds errors possible in your program. It's also incredibly useful for getting nice properties like "this vector-of-vectors representation of a matrix is not ragged" confirmed at compile time... something that even an advanced non-dependently typed language like Haskell or OCaml is (mostly) strictly in the domain of runtime checking.