[Haskell-cafe] Safe Haskell?

[Richard Eisenberg]

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.

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.

See also https://www.reddit.com/r/haskell/comments/msa3oq/safe_haskell/gv8vph9/ <https://www.reddit.com/r/haskell/comments/msa3oq/safe_haskell/gv8vph9/>, where I make similar, if not as evocative, comments.

Thanks much for the input here!
Richard

> On Apr 20, 2021, at 9:19 AM, Bertram Felgenhauer via Haskell-Cafe <haskell-cafe at haskell.org> wrote:
> 
> Bertram Felgenhauer via Haskell-Cafe wrote:
>> Unless the use case for which SafeHaskell was designed is common
>> (and the replies here indicate that it's not), this is hard to
>> justify.
> 
> The feedback here is not wholly representative.
> 
> There's a reddit thread [1] where djdlc points out
> 
>  https://uniprocess.org/effects.html
> 
> This is interesting because it demonstrates that the notion of safety
> can be *refined* from its use by the `base` library in the context of
> DSLs, because one can express which notion of safety applies through
> types, and confine the code that is ultimately executed through the
> type system.
> 
> Obviously this will still break down when the type system is subverted
> as in
> 
>  https://gitlab.haskell.org/ghc/ghc/-/issues/9562
> 
> which Richard pointed out, or
> 
>  https://gitlab.haskell.org/ghc/ghc/-/issues/19287
> 
> which wz1000 demonstrated on IRC. But these are terrible bugs anyway;
> it's just that SafeHaskell boosts their implact from code that people
> shouldn't write to a potential security issue. Is anybody maintaining
> a list of these type system unsoundness issues?
> 
> Apparently some people also enjoy the extra code discipline that
> producing Safe code requires (link by gentauro (=djdlc) on Freenode):
> 
>  http://blog.stermon.com/articles/2019/02/21/the-main-reason-i-use-safe-haskell-is-restriction.html
> 
> Cheers,
> 
> Bertram
> 
> 
> [1] https://reddit.com/r/haskell/comments/msa3oq/safe_haskell/
> or https://teddit.net/r/haskell/comments/msa3oq/safe_haskell/
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210420/77b672a9/attachment.html>