On Friday, 27 February 2015 at 08:34:24 UTC, Kagamin wrote:
>@safe is supposed to provide safety, if you can give an example
> when it doesn't, you can report a bug. There are indeed bugs in implementation of safety, like escaping of local variables, but they are supposed to be fixed eventually.

The bug is in using an approach that does not use proofs.

If you can't give an example of unsafety easily, that's already quite important. Compare to C, where one can provide such an example easily. If you want to write a mathematical prover, that won't hurt, though such tools don't need language support, lints and provers were written even for C.

On Friday, 27 February 2015 at 09:33:43 UTC, Kagamin wrote:
> If you can't give an example of unsafety easily, that's already quite important. Compare to C, where one can provide such an example easily.

Yes, that is true. Also, if you are conservative in C++ you also get pretty good safety with unique_ptr etc. So weak memory safety is ok, but then I also think it is ok to provide @trusted convenience since you are already saying that the programmer is competent:

unsafe_malloc!T()
unsafe_free!T()
unsafe_memmove!T()
unsafe_mmap…

> If you want to write a mathematical prover, that won't hurt, though such tools don't need language support, lints and provers were written even for C.

Yep. But what I meant is that a type system (including memory safety) ought to be proven sound. I.e:

1. You construct a simple language/type-system P and prove that P is sound and safe.
2. You construct a transform T(x) that can transform language D into x.

=> D is proven safe.

On 2/27/15 3:29 AM, Kagamin wrote:
> On Thursday, 26 February 2015 at 16:25:59 UTC, Steven Schveighoffer wrote:
>> However, we have an issue here. At any point inside the code, you
>> could do:
>>
>> oldcount = count;
>>
>> And now, there is still potentially a dangling pointer somewhere. This
>> means every place count is used must be checked. In this case, all
>> uses of count have to be re-checked when the file is edited.
>>
>> Because count leaks the memory details of the trusted call to free (In
>> other words, the fact that count, or any copy of it, can become a
>> dangling pointer), I believe every call in that type that deals with
>> count should be marked trusted.
>
> The counter is freed in the destructor, nothing can happen after that.

So the code is now etched in stone and cannot be changed? Is there an attribute for that? :P

-Steve

On Friday, 27 February 2015 at 10:49:25 UTC, Ola Fosheim Grøstad wrote:
> 2. You construct a transform T(x) that can transform language D into x.
>
> => D is proven safe.

Eh:

2. You construct a transform T(x) that can transform programs in language D into P...

On Friday, 27 February 2015 at 10:49:25 UTC, Ola Fosheim Grøstad wrote:
> On Friday, 27 February 2015 at 09:33:43 UTC, Kagamin wrote:
>> If you can't give an example of unsafety easily, that's already quite important. Compare to C, where one can provide such an example easily.
>
> Yes, that is true. Also, if you are conservative in C++ you also get pretty good safety with unique_ptr etc. So weak memory safety is ok, but then I also think it is ok to provide @trusted convenience since you are already saying that the programmer is competent:
>
> unsafe_malloc!T()
> unsafe_free!T()
> unsafe_memmove!T()
> unsafe_mmap…

The programmer, who wrote the trusted code is competent... or rather was competent, when he was writing the code. The problem is in cognitive load, not in competence. http://dlang.org/safed.html - did you read this?

>> If you want to write a mathematical prover, that won't hurt, though such tools don't need language support, lints and provers were written even for C.
>
> Yep. But what I meant is that a type system (including memory safety) ought to be proven sound. I.e:
>
> 1. You construct a simple language/type-system P and prove that P is sound and safe.
> 2. You construct a transform T(x) that can transform language D into x.
>
> => D is proven safe.

The compiler doesn't prove the type system, only enforces it.

On Friday, 27 February 2015 at 14:52:56 UTC, Steven Schveighoffer wrote:
>> The counter is freed in the destructor, nothing can happen after that.
>
> So the code is now etched in stone and cannot be changed? Is there an attribute for that? :P

Changes introduces in the destructor shouldn't affect other code, because nothing can happen after the destructor.

On 3/2/15 3:38 AM, Kagamin wrote:
> On Friday, 27 February 2015 at 14:52:56 UTC, Steven Schveighoffer wrote:
>>> The counter is freed in the destructor, nothing can happen after that.
>>
>> So the code is now etched in stone and cannot be changed? Is there an
>> attribute for that? :P
>
> Changes introduces in the destructor shouldn't affect other code,
> because nothing can happen after the destructor.

Then you didn't grok my point:

(()@trusted => count = new int)();

...

someOtherMember = count; // no @trusted needed here!

...

auto x = rcarray.someOtherMember; // oops, details leaked

...

~this() { ... /* destroy count via trusted */ }

...

*x += 1; // oops, still have a dangling pointer, and this can be @safe

The point is that, EVERY change to the @safe code inside RCArray has to be reviewed with this consideration (i.e. see if it makes a copy of count). And that means @safe code needs to be reviewed for safety -- something Walter does not want.

-Steve

Hmm... that means in OOP class is a unit of safety instead of a method, but it also applies to free methods, which access static members.

If one wants to prevent a leak, then counter can be wrapped
---
struct Unsafe(T)
{
   private T _payload;
   T payload() @system { return _payload; }
   alias payload this;
}
---
And somehow disallow Unsafe template in safe function signatures, then having
Unsafe!(int*) _counter;
would be ok?