[Haskell-cafe] Safe Haskell?

[Ryan Yates]

Hi Richard,

To add another place I think Safe Haskell is useful:

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.

Thanks for your work getting this discussion rolling,

Ryan

On Tue, Apr 20, 2021 at 4:54 PM Richard Eisenberg <rae at richarde.dev> wrote:

> 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/,
> 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.
>
>
> _______________________________________________
> 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/20210421/455f8ca7/attachment.html>