[jroesch]

It is not a "strong" statement to say that some Haskell code is backed by proofs. There is Wadler's Theorems for free![1] which allows one to reason about pure function's behavior purely from type signatures. As well GHC supports various features that enables one to encode some dependent typing[2] constructs.

Allowing the type of value to to depend on the value itself. A common example being a list that can expresses whether it is empty or not in its type. These types allow one to write functions with signatures like: `safeHead :: SafeList a NonEmpty -> a`. Uses of this function will fail to compile if I can not prove that my list will always be non-empty.

Combine this with the well known Curry-Howard Correspondence [3] which shows that types have a direct correspondence to proofs. The logical extension of this is computer theorem proving languages like Coq, Agda, Epigram, Idris.

For example Coq[4] uses a dependently typed lambda calculus as its proof term language, and sees wide spread use in the formal verification of software. It is not a stretch to say that less powerful types systems like Haskell's allow us to encode some forms of proof. If you view the type checker as an proof checker, one provides propositions to it (in the form of types) and then supplies proof (in the form of terms). These can be trivial propositions like `a :: Int`, which in Haskell there are 2^31 correct answers.

[1] (http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf)

[2] (http://en.wikipedia.org/wiki/Dependent_type)

[3] (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...)

[4] (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...)

[tmhedberg]

I'm aware of dependent types and, more generally, the strong undercurrent of emphasis on provable correctness in the Haskell community at large. I don't disagree at all with what you wrote, but it's not what I was referring to with my comment.

My disagreement was specifically with the implied claim that it can be mathematically proven that Haskell code is easier to maintain than code written in other languages. That has indeed been my experience with Haskell, but I do not think it is directly provable. What seems easy for me may be stupefyingly difficult or confusing for someone else.

"How easy something is" is not really a quantifiable measurement; it is a subjective experience. As chongli points out, however, there are related measurements that can be taken, such as cyclomatic complexity, and those at least seem to be correlated with ease of maintenance. So perhaps I'm just being overly pedantic!

[jroesch]

I misread your comment, usually people challenge that point. I totally agree that it is difficult to talk about maintainability in an objective fashion, but there is something to be said about having as many of your assumptions in your codebase vs. your test suite. My experiences working in a Ruby code base is that many assumptions have been encoded in the tests, and not notated in the main code base. When those assumptions change there is a large burden on the programmer of having to unify ad-hoc assumptions from both the test cases and main code base. Validating whether those assumptions still hold, or if it is a test from 3 years ago, and has only been vacuously passing.

I found working in a big Ruby code base that this required spending a non trivial amount of time unifying the two. In that regard by minimizing the amount of test code one has to write and maintain I would argue that maintainability goes up. I've also seen a lot of FP practitioners boasting about relatively low test to code ratios, while in the Ruby world often times you have at least 2x test code, since often times you even have to validate assumptions like `object.responds_to? :foo`.