Contradictory justification for status quo

[via Digitalmars-d]

On Friday, 27 February 2015 at 21:19:31 UTC, Andrei Alexandrescu 
wrote:
> On 2/27/15 1:07 PM, H. S. Teoh via Digitalmars-d wrote:
>> What about this, if we're serious about @safe 
>> actually*guaranteeing*
>> anything: after 2.067 is released, we reimplement @safe by 
>> making it
>> reject every language construct by default.
>
> I don't think this is practical. It's a huge amount of work 
> over a long time.

That's easy enough to solve, though. The new behaviour can at 
first be opt-in, enabled by a command-line flag (like we already 
do with -dip25). We have an entire release cycle, or longer if we 
need that, to get at least Phobos and druntime to compile. Once 
that is done, people can test their own code with it, and it can 
be enabled on the auto-tester by default.

When some time has passed, we invert the switch - it's then 
opt-out. People can still disable it if they just want to get 
their code to compile without fixing it (or reporting a bug if 
it's our fault). Finally, the old behaviour can be removed 
altogether.

>
> Besides, even with that approach there's still no guarantee; 
> implementation bugs are always possible in either approach.
>

As H.S. Teoh said, these can be detected by git bisect.

> I think the closest thing to what you're after is progress and 
> preservation proofs on top of a core subset of the language. It 
> would be great if somebody wanted to do this.

Wouldn't that effectively mean introducing another kind of 
`@safe`, that only allows to use said core subset? Or a compiler 
switch? How else would it be practicable?