DIP74 - where is at?

[Ola Fosheim Grøstad via Digitalmars-d]

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.