@trust is an encapsulation method, not an escape

[via Digitalmars-d]

On Friday, 6 February 2015 at 17:02:44 UTC, Wyatt wrote:
>> 3. @trusted are formally proven safe
>>
> ...by humans?

It isn't that hard for typical library code that is required to 
be non-safe.

You don't have to do better than the compiler code in terms of 
probability of slipping things through... :-P

>> 4. @trusted functions rarely change
>>
> Is this so?  Data, please.

That would be a requirement. That means you should have high 
requirements for design before allowing implementation of 
@trusted.

>
>> 5. @trusted is 0-2% of the codebase
>>
> In Phobos, you mean?  You've checked?

That would be a requirement. If you have lots of @trusted, then 
there is something wrong with the abstraction level @trusted is 
used at (or the compiler features).

>> linear type system
>>
> Time and place, man.  I'm not even sure why you're bringing 
> this up here.

What is your alternative? You need to point at the alternative. 
The only alternative I see is to drop @safe or keep @trusted or 
change the type system.

> perpetuity?  How do you separate the qualified from the 
> overconfident?  How many people need to check something 
> independently before you're reasonably certain there are no 
> mistakes?

One semi-formal proof written down. 3 qualified (education) 
independent reviews of the proof.

What makes this more difficult for the standard library than for 
the compiler internals?

> etc.  Any time you bind yourself to human process, you've 
> created a bottleneck of uncertainty.

And the alternative is?

> And that's just Phobos! You don't scale horizontally and it's 
> kind of problematic to approach this with the assumption that 
> everyone wanting to write something that even reasonably 
> approximates safe code is a mathematician.  Rather, that 
> doesn't bear out in practice at all.
>
> Bottom Line: If it can't be even partially automated, it's not 
> useful.

Then drop @safe...