<div dir="ltr">Hi Richard,<div><br></div><div>To add another place I think Safe Haskell is useful:</div><div><br></div><div>GHC's STM performs lazy validation which means it allows execution of "zombie" or "doomed" transactions, an executing transaction that has observed inconsistent reads from `TVar`s, but has not yet detected it.  Given this, unsafe operations can introduce failures when executing a transaction that would not happen executing sequentially.  I argued in my thesis that Safe Haskell is sufficient to prevent this.  That is, libraries that are safe are safe to use in transactions.<br></div><div><br></div><div>Thanks for your work getting this discussion rolling,</div><div><br></div><div>Ryan</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Apr 20, 2021 at 4:54 PM Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;">After keeping up with this thread, the reddit thread, and a Twitter thread, I started to write a GHC proposal to remove Safe Haskell. However, a conversation with Krzysztof Gogolewski (aka monoidal) and a post on reddit made me change my mind: we need to renovate Safe Haskell, not remove it. And doing so only really makes sense in the context of a larger security overhaul.<div><br></div><div>We are as a loose encampment in an open field with a few night sentries. Safe Haskell is a slightly-crumbling earthen rampart along two sides of the encampment. As such, it's really just an obstacle, and does little (but not nothing) to protect us. I was thinking to clear away the obstacle. But of course the better solution is to reinforce the rampart, build two more sides of it, and create a proper defensive position. This will be hard, and I do not propose to take charge of such an act now. But I recognize that the existing structure naturally forms part of this greater whole.</div><div><br></div><div>See also <a href="https://www.reddit.com/r/haskell/comments/msa3oq/safe_haskell/gv8vph9/" target="_blank">https://www.reddit.com/r/haskell/comments/msa3oq/safe_haskell/gv8vph9/</a>, where I make similar, if not as evocative, comments.</div><div><br></div><div>Thanks much for the input here!</div><div>Richard</div><div><div><div><div><div><br><blockquote type="cite"><div>On Apr 20, 2021, at 9:19 AM, Bertram Felgenhauer via Haskell-Cafe <<a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a>> wrote:</div><br><div><div>Bertram Felgenhauer via Haskell-Cafe wrote:<br><blockquote type="cite">Unless the use case for which SafeHaskell was designed is common<br>(and the replies here indicate that it's not), this is hard to<br>justify.<br></blockquote><br>The feedback here is not wholly representative.<br><br>There's a reddit thread [1] where djdlc points out<br><br>  <a href="https://uniprocess.org/effects.html" target="_blank">https://uniprocess.org/effects.html</a><br><br>This is interesting because it demonstrates that the notion of safety<br>can be *refined* from its use by the `base` library in the context of<br>DSLs, because one can express which notion of safety applies through<br>types, and confine the code that is ultimately executed through the<br>type system.<br><br>Obviously this will still break down when the type system is subverted<br>as in<br><br>  <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/9562" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/9562</a><br><br>which Richard pointed out, or<br><br>  <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/19287" target="_blank">https://gitlab.haskell.org/ghc/ghc/-/issues/19287</a><br><br>which wz1000 demonstrated on IRC. But these are terrible bugs anyway;<br>it's just that SafeHaskell boosts their implact from code that people<br>shouldn't write to a potential security issue. Is anybody maintaining<br>a list of these type system unsoundness issues?<br><br>Apparently some people also enjoy the extra code discipline that<br>producing Safe code requires (link by gentauro (=djdlc) on Freenode):<br><br>  <a href="http://blog.stermon.com/articles/2019/02/21/the-main-reason-i-use-safe-haskell-is-restriction.html" target="_blank">http://blog.stermon.com/articles/2019/02/21/the-main-reason-i-use-safe-haskell-is-restriction.html</a><br><br>Cheers,<br><br>Bertram<br><br><br>[1] <a href="https://reddit.com/r/haskell/comments/msa3oq/safe_haskell/" target="_blank">https://reddit.com/r/haskell/comments/msa3oq/safe_haskell/</a><br> or <a href="https://teddit.net/r/haskell/comments/msa3oq/safe_haskell/" target="_blank">https://teddit.net/r/haskell/comments/msa3oq/safe_haskell/</a><br>_______________________________________________<br>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>Only members subscribed via the mailman list are allowed to post.</div></div></blockquote></div><br></div></div></div></div></div>_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>