On Friday, 6 February 2015 at 15:14:14 UTC, Wyatt wrote:
So from my perspective, calling this situation "completely
impractical" reveals a stunning gift for understatement. Is
this really the best we can do after however many years?
Because it blows.
The current @trusted semantics (and accompanying politics) make
it exceedingly clear that @safe is meaningless for anything
beyond trivial, one-off tools that will never receive
maintenance.
I don't get this. If:
1. @safe actually works.
2. @trusted sections are written without dependencies
3. @trusted are formally proven safe
4. @trusted functions rarely change
5. @trusted is 0-2% of the codebase
Then how is this more work than implementing something like a
linear type system that is both tedious for the programmer and
has taken Rust 8 years to get into working shape...?
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.
The resources we obviously don't have is experts on type systems
and automated proof and verification engines.
