@trust is an encapsulation method, not an escape

[Wyatt via Digitalmars-d]

On Friday, 6 February 2015 at 15:48:45 UTC, Ola Fosheim Grøstad 
wrote:
>
> 2. @trusted sections are written without dependencies
>
This really won't happen unless statically enforced because 
humans are involved.

> 3. @trusted are formally proven safe
>
...by humans?

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

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

2% in my world is already thousands of lines of code, and I'm far 
from having the largest of maintenance burdens.  Get it to a 
small fraction of a percent and then maybe we can talk.

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

> Jonathan recently said he would like to volunteer some, and he 
> has mentioned a background with math/proofs. If he is willing 
> to do safety review, then so I am, then so will someone else 
> who feel like refreshing their training in program 
> verification... Use the resources you have. Those resources, we 
> do have, I think. Unused.
>
That's great; thanks for that.  Seriously.  But to my mind, that 
adds a whole new stack of concerns.  How many people do you think 
you'll need to absorb the patch flow to Phobos?  In 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?  etc.  Any time you 
bind yourself to human process, you've created a bottleneck of 
uncertainty.

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.

-Wyatt