Haskell is often touted as the language to do proofs in. (Before they start recomnding Agda, Idris or Coq). However, is this piece of code not potentially problematic or am I understanding the concept wrong?

x :: Int -> Int
x n
 | x == 0 = error "Error"
 | otherwise = n   1

As far as I understand this is not very good for checking proofs(since returning Int is not mandatory here.)
Is there a way we could solve this?

As far as I understand, the other aforementioned languages avoid this.[1] I do not understand how. Is it simply because of the stricter type-system or some other guarantee provided by the language?

So far I have looked at the language documentations at a high level but found nothing.

[1] = https://www.reddit.com/r/haskell/comments/9toh6b/comment/e8y4gzi/?utm_source=share&utm_medium=web2x&context=3

CodePudding user response：

If somebody recommended that you do in proofs in Haskell, ask for your money back. (But be sure to double check you understood. Maybe they said to do proofs about Haskell and your memory is bad!)

You are correct: it is not very good for checking proofs. Haskell is, as a logic, inconsistent. That means you can prove anything. There's a quote from another smart Haskeller that I think of from time to time; I can't find the exact wording, but it goes something like "programmers are logicians that spend all their time proving trivial theorems in overly complicated ways". This is just another example of that; a real logician, once they found an inconsistency, would stop trying to prove other things because they've already finished proving everything.

The languages you mention (Coq, Agda, and Idris) get around this problem by requiring not just a proof of the thing you want to prove, but also a proof that the proof you wrote finishes evaluating eventually. (Mostly that second proof is implicitly enforced by restricting the class of proofs you can write, but people are extending the class of proofs that pass the automatic checks all the time.) Once you demand termination, it is no longer possible to implement error :: String -> a in the first place. (Except as a compiler primitive, of course... so they just don't do that.)