@trust is an encapsulation method, not an escape

[via Digitalmars-d]

On Friday, 6 February 2015 at 15:14:14 UTC, Wyatt wrote:
> So from my perspective, calling this situation "completely 
> impractical" reveals a stunning gift for understatement.  Is 
> this really the best we can do after however many years?  
> Because it blows.
>
> The current @trusted semantics (and accompanying politics) make 
> it exceedingly clear that @safe is meaningless for anything 
> beyond trivial, one-off tools that will never receive 
> maintenance.

I don't get this. If:

1. @safe actually works.

2. @trusted sections are written without dependencies

3. @trusted are formally proven safe

4. @trusted functions rarely change

5. @trusted is 0-2% of the codebase

Then how is this more work than implementing something like a 
linear type system that is both tedious for the programmer and 
has taken Rust 8 years to get into working shape...?

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.

The resources we obviously don't have is experts on type systems 
and automated proof and verification engines.