Despite what the fanatical constructivists (as opposed to the ones who simply think it's pragmatically nice) seem to want us to think, it turns out that you can prove interesting things with LEM (AKA call/cc) and classical logic.
Yes haskell's `bottom` breaks soundness, but that doesn't mean you need to take away some capability from the language. You just need to extend the language with a totality checker for the new proof fragment.
Idris absolutely is a general-purpose functional language in the ML family. It is Haskell, but boosted with dependent types.
While reading TFA I thought the theorem stuff deserved its own category, but I guess it's a specialization within an ur-family (several), rather than its own family?
It definitely sounds like it deserves its own category of programming language, though. The same way Lojban has ancestry in many natural languages but is very much doing its own thing.
But I think that the theorem prover that excels most at regular code is actually Lean. The reason I think that is because Lean has a growing community, or at least is growing much faster than other similar languages, and for regular code you really need a healthy ecosystem of libraries and stuff.
Anyway here an article about Lean as a general purpose language https://kirancodes.me/posts/log-ocaml-to-lean.html
> 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
What I meant is that the part of Idris that lets people prove theorems is the non-total part
But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages