safe vs. unsafe (Was: Haskell Platform proposal: Add the vector package)

[Simon Marlow]

On 14/07/2012 13:27, Brandon Allbery wrote:
> On Sat, Jul 14, 2012 at 3:16 AM, Henning Thielemann
> <lemming at henning-thielemann.de <mailto:lemming at henning-thielemann.de>>
> wrote:
>
>     On Fri, 13 Jul 2012, Brandon Allbery wrote:
>
>         And now I'm having a "so what's the point?" moment?  All this
>         effort so we can just mark random stuff as
>         Trusted anyway?
>
>
>     Today we have 'unsafePerformIO'. So if we praise the merits of
>     Haskell's strong type system and then mention 'unsafePerformIO' the
>     audience will ask "so what's the point of type safety then?" Well,
>     the point is that unsafePerformIO is strongly discouraged and every
>     use of it should be considered carefully.
>
>
> We've just been told *not* to consider carefully for purposes of marking
> a module as Trustworthy; an argument based on considering carefully is
> not relevant.

Perhaps I gave the wrong impression: of course you should carefully 
consider every use of unsafePerformIO, just as we already do.  You 
should only mark an interface as Trustworthy if you really believe that 
it is.

How firm should your belief be?  Well, you could ask the same question 
about GHC's type system - do we really believe that if a program passes 
the type system then it can't crash?  We haven't formally verified the 
type system or its implementation, after all.  Similarly, does GHC's 
garbage collector work?  In the absence of formal verification, it's all 
just code that we have to trust.  Trustworthy Haskell code has exactly 
the same status, and the degree to which you trust any piece of code is 
up to you.

What's new in Safe Haskell is that we can now have Haskell code that you 
do *not* have to trust, as long as you trust some other things: 
including the implementation of Safe Haskell, GHC's type system and RTS, 
and any Trustworthy Haskell libraries that are in the dependency chain.

Cheers,
	Simon