And I'll add this:
Please do not turn the compiler into a inadequate verification
tool. The compiler should do what it can do well, but what it
cannot do it should not do at all and leave to an external
verification tool.
@trusted basically tells the compiler "this is beyond your
capability so we left it to someone else".
Third parties should be able to provide incrementally improved
verification tools, for various purposes, without mandating
language or compiler changes.
So what you want from the language is simple clean semantics and
reasonable best practice annotations for verification that can be
extended based on the needs in a particular environment.
