On Friday, 6 February 2015 at 17:02:44 UTC, Wyatt wrote:
3. @trusted are formally proven safe
...by humans?
It isn't that hard for typical library code that is required to
be non-safe.
You don't have to do better than the compiler code in terms of
probability of slipping things through... :-P
4. @trusted functions rarely change
Is this so? Data, please.
That would be a requirement. That means you should have high
requirements for design before allowing implementation of
@trusted.
5. @trusted is 0-2% of the codebase
In Phobos, you mean? You've checked?
That would be a requirement. If you have lots of @trusted, then
there is something wrong with the abstraction level @trusted is
used at (or the compiler features).
linear type system
Time and place, man. I'm not even sure why you're bringing
this up here.
What is your alternative? You need to point at the alternative.
The only alternative I see is to drop @safe or keep @trusted or
change the type system.
perpetuity? How do you separate the qualified from the
overconfident? How many people need to check something
independently before you're reasonably certain there are no
mistakes?
One semi-formal proof written down. 3 qualified (education)
independent reviews of the proof.
What makes this more difficult for the standard library than for
the compiler internals?
etc. Any time you bind yourself to human process, you've
created a bottleneck of uncertainty.
And the alternative is?
And that's just Phobos! You don't scale horizontally and it's
kind of problematic to approach this with the assumption that
everyone wanting to write something that even reasonably
approximates safe code is a mathematician. Rather, that
doesn't bear out in practice at all.
Bottom Line: If it can't be even partially automated, it's not
useful.
Then drop @safe...
