@trust is an encapsulation method, not an escape

[via Digitalmars-d]

On Friday, 6 February 2015 at 18:51:34 UTC, Steven Schveighoffer 
wrote:
> My point was that if you have @trusted escapes inside a 
> function, whether it's marked @safe or not, you still have to 
> review the whole function. If the compiler disallowed this 
> outright, then you don't have that issue.

Ok, I also prefer that @trusted only apply to whole functions. I 
don't agree with the argument, but let's leave it at that ;-).

> Separating the trusted code from the safe code via an API 
> barrier has merits when it comes to code review.

Yes. And I actually don't think @trusted functions in Phobos 
should contain version() or other forms for conditional 
compilation since that makes it much harder to reason about.

> I see the point now that making sure @safe functions don't have 
> escapes has the advantage of not requiring *as much* review as 
> a @system or @trusted function. I am leaning so much towards 
> H.S. Teoh's solution of making @trusted safe by default, and 
> allowing escapes into @system code. That seems like the right 
> abstraction.

Just to make sure that I got this right:

I don't really understand why you need to escape to @system from 
@trusted. Isn't @trusted the same as @system but with a seal that 
says that it has been manually verified to be memory safe?  
@system simply allows the same internal semantics as @trusted but 
with no such declared guarantee to the caller?

Except that in @system you could potentially switch the stacks 
and do other unsafe operations that are not brought back to 
normal before leaving the system context... In @trusted you are 
required to restore the context to normal before returning.

So in the type system you only have @safe and @system, @trusted 
is just @safe with flexible manual verification rather than the 
limited automated verification DMD is capable of. Thus you only 
need to export @safe vs @system for separate compilation...?

Isn't that how it is supposed to work already?

> I see what you mean, but there are also really dumb things that 
> people miss that a compiler won't. Having a mechanical set of 
> eyes in addition to human eyes is still more eyes ;)

Well, if you can come up with something sound. The way I see it, 
@trusted functions are allowed to create a new context on entry 
as long as it restores the previous context before exiting.

This essentially means that what is @safe before entering 
@trusted no longer can be guaranteed to be safe. The floating 
point unit might work differently and result in memory unsafe 
operations etc etc.

So calling @safe from @trusted means that you are calling @safe 
as if it was @system. And therefore @safe code called from 
@trusted has to be proven correct just like @system code called 
from @trusted.

> The way reviews are done isn't anything the language can 
> require. Certainly we can provide guidelines, and we can 
> require such review processes for phobos and druntime.

Yes, in Phobos you need to impose additional stricter guarantees 
in order to support the formal review process and ensure that the 
formal review cannot be broken without a new review taking place. 
And yes, that is a process requirement, not a language 
requirement. A different process might impose other 
requirements...

I think you will have to define such a process though, because I 
don't think there is a solution for fully automated verification 
for D without going for a much more complex type system and 
mechanics (which I actually think is out of reach unless 
everything is designed around it).

Fortunately with 3 reviewers you can do quite well if the proof 
is available and they work independently without sharing results 
before everyone is done. If each reviewer has a 10% chance of 
failure then you end up with only 0.1% chance of all of them 
failing... So it is possible to get decent results with a formal 
process in place.

Complicated @trusted code (hard to prove safe) should be rejected 
and unnecessary @trusted code should be fixed in the compiler 
optimizer or by adding language features (like SIMD).