alt Hacker NewsTheorem proving and complex types are like extensions on an otherwise ordinary language:
- Agda, Idris, etc. are functional languages extended with complex types
- Isabelle, Lean, etc. are functional languages extended with complex types and unreadable interactive proofs
- Dafny etc. are imperative languages extended with theorems and hints
- ACL2 is a LISP with theorems and hints
Related, typeclasses are effectively logic programming on an otherwise functional/imperative language (like traits in Rust, mentioned in https://rustc-dev-guide.rust-lang.org/traits/chalk.html).
> Agda, Idris, etc. are functional languages extended with complex types
I think they are not. No amount of type level extensions can turn a regular functional language like Haskell into something suitable for theorem proving. Adding dependent types to Haskell, for example, doesn't suffice. To build a theorem prover you need to take away some capability (namely, the ability to do general recursion - the base language must be total and can't be Turing complete), not add new capabilities. In Haskell everything can be "undefined" which means that you can prove everything (even things that are supposed to be false).
There's some ways you can recover Turing completeness in theorem provers. You can use effects like in F* (non-termination can be an effect). You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean. But still, you need the base terms to be total, your logic is done in the fragment that isn't Turing complete, everything else depends on it.