@trust is an encapsulation method, not an escape

[via Digitalmars-d]

On Friday, 6 February 2015 at 14:00:24 UTC, Atila Neves wrote:
> 1. Agree with H S Teoh on the maintainability aspect. Depending 
> on humans reviewing the code is never going to work out.

Of course it can work out. You need a formalized process and a 
group of people with training in math or comp.sci to do the 
review.

Proving memory safety for a single function in a semi-formal 
manner is not like proving full correctness.

I suggest the following:

1. @trusted should only be used on high priority code (not to 
gain minor speed ups)

2. @trusted code should always carry the safety-proof as embedded 
comments

3. @trusted templates should carry the most stringent type 
constraints (and proof required to weaken them)

4. At least 3 reviewers with knowledge of compsci/math MUST 
verify the soundness of the proof.

5. Have a list of volunteers that are called in by email to 
review @trusted code.

If only 2% is @trusted then this should work out fine. The 
alternative is to give up @safe completely or completely change 
the typesystem.