<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 3 Jan 2017, at 21:38, Artyom <<a href="mailto:yom@artyom.me" class="">yom@artyom.me</a>> wrote:</div><br class="Apple-interchange-newline"></blockquote> <stuff elided><br class=""><blockquote type="cite" class=""><div class="">
<meta content="text/html; charset=utf-8" http-equiv="Content-Type" class="">
<div bgcolor="#FFFFFF" text="#000000" class=""><p class="">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.</p><div class="">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.</div></div></div></blockquote><div><br class=""></div>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".</div><div><br class=""></div><div>The rapid theory calculator has proved crucial to my recent work, where testing the theory by calculation was rapidly becoming intractable. However developing the calculator itself was only itself feasible because I could play fast and loose with my code. Just like Artyom, if I had had to fight the compiler and Prelude, I would have lost the will to live....</div><div><br class=""></div><div>Perhaps I'm an outlier too ? ;-)</div><div><br class=""></div><div>[1] <a href="https://arxiv.org/abs/1410.8216v1" class="">https://arxiv.org/abs/1410.8216v1</a></div><div>[2] <a href="https://www.scss.tcd.ie/andrew.butterfield/DRAFTS/preprints/UTPCalc-UTP2016-MAIN.pdf" class="">https://www.scss.tcd.ie/andrew.butterfield/DRAFTS/preprints/UTPCalc-UTP2016-MAIN.pdf</a></div><div> (to appear in LNCS 10134, Feb 2017<br class=""></div><br class=""><div class="">
<div class=""><div class="">Andrew Butterfield</div><div class="">School of Computer Science & Statistics</div><div class="">Trinity College</div><div class="">Dublin 2, Ireland</div></div>
</div><div class=""><br class=""></div><div class=""><br class=""></div>
<br class=""></body></html>