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

newer
split package HP proposal, round 2

older
Proposal: add an order-reversing...

Simon Marlow

13 Jul 2012 13 Jul '12

6:26 p.m.

On 13/07/12 21:18, Heinrich Apfelmus wrote:

...

Simon Marlow wrote:

...
Hi Thomas,

All these questions are answered by the Haskell Symposium paper, which we'll post very shortly. FYI, the FFI is mostly safe, as long as you declare foreign imports to have an IO result type (otherwise it's unsafePerformIO, and hence unsafe). Unsafety is not viral: as soon as you have a safe API, you can declare its implementation to be Trustworthy, and then it is usable from safe code.

How strict are the requirements for Trustworthy code? For instance, my reactive-banana library uses observable sharing, which is inherently Unsafe. Of course, I think that my library is still Safe, but I have no formal proof of this "fact". I have two options:

1. Mark my library as Trustworthy even though I don't have sufficient proof. This severely weakens the guarantees of Safe Haskell. 2. Mark my library as Unsafe. But then people can't use it to write Safe code and will complain.

The trouble is that I have a strong incentive to solve the problem arising from 2 by doing 1. Oops.

The idea is that you do (1). All your clients get to use Safe, and nobody is obliged to use your code in a security-critical setting unless they want to. (I could write a lot more, but I've written too much about this already today. Good night!) Cheers, Simon

Show replies by date

Brandon Allbery

13 Jul 13 Jul

6:58 p.m.

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

On Fri, Jul 13, 2012 at 6:26 PM, Simon Marlow wrote:

...

On 13/07/12 21:18, Heinrich Apfelmus wrote:

...
1. Mark my library as Trustworthy even though I don't have sufficient proof. This severely weakens the guarantees of Safe Haskell. 2. Mark my library as Unsafe. But then people can't use it to write Safe code and will complain.

The trouble is that I have a strong incentive to solve the problem arising from 2 by doing 1. Oops.

The idea is that you do (1).

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? -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Thomas Schilling

7:50 p.m.

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

On 13 July 2012 23:58, 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?

Well, the use of the term "Trustworthy" seems off. It really means "You need to trust this module". Maybe it would better be called "TrustNeeded". Trust is something only you can decide upon (though possibly based on what other people trust, too). I'm still not convinced that it's going to be practical enough for applications such as an online Haskell evaluator. I think they point out in the paper that their definition of "safe" /= "secure".

Wolfgang Jeltsch

20 Jul 20 Jul

6:29 a.m.

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

Am Samstag, den 14.07.2012, 00:50 +0100 schrieb Thomas Schilling:

...

On 13 July 2012 23:58, 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?

Well, the use of the term "Trustworthy" seems off. It really means "You need to trust this module".

If a module is declared “Trustworthy”, it means that the author thinks this module provides a safe interface, despite using unsafe features internally. If you then declare in your local installation that the package of that module is trustworthy, you say that you trust the author’s opinion about trustworthiness. Both things together make the module effectively trusted. Best wishes, Wolfgang

Henning Thielemann

14 Jul 14 Jul

3:16 a.m.

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

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. I actually check packages that I install for the use of unsafePerformIO. For this reason I rejected to use for instance the cmdargs package because in my opinion unsafePerformIO is not necessary for implementing a command line argument parser. I have learnt that a safer interface was added since then, but the unsafe one still exists. SafeHaskell could help to make explicit what parts of the package are "clean" and which ones are "hacks". So I think SafeHaskell could be a way to locate problems in code faster. Since a Haskell 98 program without unsafePerformIO and friends cannot crash, a crash can be only caused by Unsafe code.

Brandon Allbery

8:27 a.m.

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

On Sat, Jul 14, 2012 at 3:16 AM, Henning Thielemann < lemming@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. -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Yitzchak Gale

15 Jul 15 Jul

7:48 a.m.

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

Posting to libraries only. 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?

Henning Thielemann wrote:

...

...
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.

In the vast majority of cases it's a no-brainer that your module can be marked at least Trustworthy, if not Safe. The paper gives well-defined simple criteria for when there might be a problem. In the rare instance where there might be a problem, then yes, you do devote some thought to it. And if you get it wrong, it's just a bug that needs to be fixed, like anything else. Safe Haskell automates the kind of sanity check that we all know we should be doing for everything we write, but have been neglecting because it takes too much time. That makes it practical, not just theoretically possible. That's a huge value. And it's very easy to implement, hardly any effort. See Simon's paper. Thanks, Yitz

Simon Marlow

16 Jul 16 Jul

7:31 a.m.

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

On 14/07/2012 13:27, Brandon Allbery wrote:

...

On Sat, Jul 14, 2012 at 3:16 AM, Henning Thielemann mailto:lemming@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

Henning Thielemann

18 Jul 18 Jul

6:47 a.m.

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

On Sat, 14 Jul 2012, Henning Thielemann wrote:

...

So I think SafeHaskell could be a way to locate problems in code faster. Since a Haskell 98 program without unsafePerformIO and friends cannot crash, a crash can be only caused by Unsafe code.

Shortly after I wrote this, I noticed that I was wrong. IO also allows you to crash in many ways. Thus I have to say: A Haskell 98 program without IO, unsafePerformIO and friends cannot crash. I first saw the UNSAFE feature in Modula-3. Modula-3 does not have referential transparent functions and does not distinguish between IO functions and non-IO functions. So what does UNSAFE mean for Modula-3? Actually, Modula-3 programs with only SAFE modules cannot crash, because pointer arithmetic and typecasts (LOOPHOLE) are only allowed in UNSAFE modules.

4688

Age (days ago)

4695

Last active (days ago)

List overview

Download

8 comments

6 participants

participants (6)

Brandon Allbery
Henning Thielemann
Simon Marlow
Thomas Schilling
Wolfgang Jeltsch
Yitzchak Gale

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

tags

participants (6)