| > It was me Yes, it was you :) > The type system helps you enforce useful invariants in your code and can make verification easier, but it's completely orthogonal to how you can prove programs correct. That's true for Java. Haskell, OTOH, constructs the entire language around verification through types and pure functions, and everything else is secondary. I don't know if the connection to C-H was made later or was a conscious design decision, but the result is the same from the user's perspective. > Theorem provers based on C-H are general-purpose logics that can be used for a lot more than just program verification We've discussed this before, and I believe those uses are too niche for the Haskell approach to gain any significant traction. > You can show that, quite literally, any "true property" of a program in your more complicated language is also true of the corresponding program in your simpler language. Of course, but that is only useful if a human programmer writing in the more "complicated" (by your definition) language would use the "simpler" subset, which, by my definition, she wouldn't do. > There's no need to solve the much, much harder (and poorly specified) problem of "what is easiest for humans". It's not a mathematical problem with a clear solution, and therefore requires no robust specification -- just like architecture (of buildings), or any other UI design problem. We learn what works through trial and error and try to do better. I find it hard to accept the point of view which considers UI to be a methematical puzzle, or, alternatively, that doesn't recognize programming languages as UIs. > but that's an entirely different problem independent of semantic considerations. From a UI design perspective, you can't separate the two, because if the user fails to interact with the machine well, you don't know if it's a matter of design or presentation unless you empirically test it. |
The type system of Haskell is far more interesting and powerful than that of Java, but I think you're overstating the difference. While Haskell's type system does allow you to do a few more things than just demonstrate restraints on your code (such as construct more expressive types and make use of type classes and polymorphism), at the end of the day the overwhelming utility of the type system is being able to more easily make guarantees about your code, just as it is in Java.
Curry-Howard only really becomes interesting once you have dependent types, and only becomes bullet-proof when your language is total. Haskell has neither property. The connection to C-H is something which might interest a large subset of Haskell programmers (who would likely take that interest into a study of Coq, Agda or Idris), but it has pretty much no bearing on the day-to-day usage of Haskell.