On 3 Jan 2017, at 21:38, Artyom <yom@artyom.me> wrote:

My personally preferred outcome – i.e. what I want Haskell to be – is a language that is fun to use while still being *possible* to make safe if needed. Thus, I'm glad that newtypes exist and can be used without that much effort. I'm glad that alternative preludes that ban partial functions could be written. I'm glad that qualified imports exist, and I also think it would be good if there was a GHC flag banning unqualified imports. I'm glad that phantom types, type families, etc all exist and are helping people write safe code that they wouldn't be able to write otherwise.
Howevev, what I feel really strongly about is that such things should not be the default. It's good that a professional Haskeller (or a team of Haskellers, or a Haskell shop, etc) can enforce safety standards if they want to, and it's good that with Haskell it's easier than with other languages, but why should those standards be forced on *all* Haskellers? Contrary to what some might believe, safety is not an ultimate goal of every Haskeller (an example being myself). I'm fine with my code failing every now and then, because the alternative is that it might not get written at all as I get tired of fighting the compiler and the Prelude.

I couldn't agree more. Ironically my main research area is that of formal methods and formal semantics, for techniques to prove software (and system) correctness. I have written a number of Haskell programs to assist me - including a GUI-based equational reason theorem prover [1] and a form of "rapid theory prototyping" calculator [2]. For the former correctness is very important, but not the latter. The problem I have to solve is that of "debugging" semantic theories that I develop - as John Rushby of SRI said back in '93: "95% of theorems are false".