Experimental languages are intended to prove a point. "Agda or Epigram or Coq" and the like are experimental as well so it seems moot to say they are the future. The question is, Is Haskell a solid foundation to build upon? The Haskell language has been brave and perhaps too brave. Everyone knew that layout could get you into trouble and so most everyone had the good sense to avoided it. With Haskell it made sense due to its emphasis on white space. In typography white space is crucial. It is helpful to clear away the clutter that fogs the mind. When it is beautiful it is easier to read. It becomes a pleasure to read. I take no issue with the two Simons for being uncompromising. This is to be admired. As layout is concerned though it was risky, I'm not ready to give up on layout. Apart from those who state objection to Haskell in that it does not behave like C. Since the paradigms are different one could expect that how things are done are different. So I'm throwing that out and them out with it. It is not a cogent criticism. There are still things that can be done, but it involves breaking with backward compatibility and doing it right this time. Near perfection is possible. You just have to want it bad enough. It is funny that you should speak of the Coq proof assistant and related projects. You don't get it do you? It isn't about kind of getting it right. It is about having a formal mathematical proof that you got it right. I'm uncertain if Haskell in its present state can deliver. With all this monkeying with the language and ad-hoc changes it won't improve things. It will just be business as usual. Though Epigram is written in Haskell I don't see it going anywhere. Coq is not written in Haskell. Most proof assistants worth their salt aren't. I think I now understand why. Haskell has a grocery list of proof assistant projects that either were abandoned or look like they were abandoned. I don't think that should be, but maybe I'm just in the minority. If you think "Agda or Epigram or Coq" is the future, why then do you hold such thoughts as "We shouldn't try too hard to get Haskell right". It doesn't follow logically. Someone has got to get it right for Epigram, et al, to get it right.