There are a relatively small number of trouble spots. They include, at least:
- No way to talk about partially initialized arrays in Rust, which leads to Vec needing "unsafe".
- Back references, which makes some kinds of trees, and of course doubly-linked lists, difficult.
Those I've mentioned before. From the discussion above, add:
- Problems around interior mutability within arrays, where you need some way to say, and prove, "a is disjoint from b", before working separately on a and b.
These are classic proof of correctness areas. It's fairly straightforward to state the conditions that have to be proven, and usually not that hard to prove them. The RustBelt crowd seems to be working on this.
Maybe they'll come up with a way to prove out conditions like that, short of grinding away by hand in Coq. Most of those problems are within reach of a fully automatic prover, like a SAT solver.
You're right, but current Rust cannot express logical preconditions in code, much less compiler-checkable proofs. Many groups are working on this via a variety of approaches, but it will take some time before there's a common standard for expressing these things as part of the Rust language itself.
I agree with Animats here, to work around typesystem issues means that the type system still isn't expressive enough to define certain proprieties in a safe way.
thread::spawn uses unsafe code. sleep uses unsafe code. Is your own example not in Rust? Are you cheating?
(And yes, the spawn version isn’t optimally concurrent. The comment was long enough without getting into that. People struggle to get examples to compile before they worry about things like this. That would be next steps.)