On Sunday, 11 October 2015 at 23:46:42 UTC, Jonathan M Davis
wrote:
@safe isn't going anywhere. And it mostly works just fine. It's
primary flaw is that it's been done via blacklisting operations
rather than whitelisting them, but that doesn't stop it from
working. It just makes the implementation more error-prone.
Has nothing with whitelisting or blacklisting, that's basically
the same thing for a finite set of features.
The real problem is that it cannot be assumed to work until
proven correct, formally. So it does not give you anything more
than a weak sanitizer would have done until such proofs have been
verified. The fact that it is difficult to be convince oneself
that you don't have holes reinforces this viewpoint.
If reasoning is difficult, you need proofs.
Walter and Andrei are completely behind @safe and are going to
be in favor of fixing any holes in it that are found, not
getting rid of it. And I don't see any reason why that can't
work or that it's a bad idea.
This has been discussed before. @trusted regions can be correct
in isolation, but it will make assumptions about what goes into
@safe regions, so when the @safe region changes @trusted regions
cannot assumed to be correct anymore. Therefore you need a prover
to prove the @trusted region to remain safe whenever you change
the surrounding @safe region. That means @trusted has to be truly
exceptional and rare and impose verfiied restrictions on the
assumptions it makes, which is not likely to happen.
This comes in conflict with the very nature of system level
programming.
