On Friday, 6 February 2015 at 15:48:45 UTC, Ola Fosheim Grøstad
wrote:
2. @trusted sections are written without dependencies
This really won't happen unless statically enforced because
humans are involved.
3. @trusted are formally proven safe
...by humans?
4. @trusted functions rarely change
Is this so? Data, please.
5. @trusted is 0-2% of the codebase
In Phobos, you mean? You've checked?
2% in my world is already thousands of lines of code, and I'm far
from having the largest of maintenance burdens. Get it to a
small fraction of a percent and then maybe we can talk.
linear type system
Time and place, man. I'm not even sure why you're bringing this
up here.
Jonathan recently said he would like to volunteer some, and he
has mentioned a background with math/proofs. If he is willing
to do safety review, then so I am, then so will someone else
who feel like refreshing their training in program
verification... Use the resources you have. Those resources, we
do have, I think. Unused.
That's great; thanks for that. Seriously. But to my mind, that
adds a whole new stack of concerns. How many people do you think
you'll need to absorb the patch flow to Phobos? In 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? etc. Any time you
bind yourself to human process, you've created a bottleneck of
uncertainty.
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.
-Wyatt
