[Araq]

Disclaimer: I'm the lead designer of Nim.

pcwalton's remark is excellent but "automated proof technology" is not a well defined term. What I mean by this is that it goes beyond what a traditional type checker can do. I don't think Rust can do exactly the same things via its borrow checking and its iterators, but I might be wrong. Note that the very same analysis also proves your index bounds are correct.

Nim's disjoint checker is so experimental that its docs are indeed very terse and we only have a couple of test cases for now. That said, the disjoint checking is restricted to the 'parallel' statement, so its complexity only affects this language construct and not the whole language. You can think of it as a macro that does additional checking.

[dbaupp]

> I don't think Rust can do exactly the same things via its borrow checking and its iterators, but I might be wrong

Reading http://nim-lang.org/manual.html#parallel-statement point by point (disclaimer, I think Nim is very cool, but safe parallelism is one of Rust's strongest points):

> Every location of the form a[i] and a[i..j] and dest where dest is part of the pattern dest = spawn f(...) has to be provably disjoint. This is called the disjoint check.

The type system guarantees disjointness when necessary: a mutable reference `&mut` is guaranteed to be the only way to access the data it points to at any given point in time and iterators over mutable references preserve this guarantee, so disjointness-for-writing is automatic.

> Every other complex location loc that is used in a spawned proc (spawn f(loc)) has to be immutable for the duration of the parallel section. This is called the immutability check. Currently it is not specified what exactly "complex location" means. We need to make this an optimization!

Rust generalises immutable to "safe to be used in parallel"; everything that is (truly) immutable satisfies this, but so do, for example, memory locations that can only be used with atomic CPU instructions, or values that are protected by a mutex. There's no way to get data races with such things, so they're safe to refer to in multiple threads.

This is captured by the Sync trait (types which can be used from multiple threads in a shared way implement it): http://doc.rust-lang.org/nightly/std/marker/trait.Sync.html

> Every array access has to be provably within bounds. This is called the bounds check.

Rust's iterators give in-bounds automatically, but there's also no restriction about requiring bounds checks or not. (What does this rule offer Nim?)

> Slices are optimized so that no copy is performed. This optimization is not yet performed for ordinary slices outside of a parallel section. Slices are also special in that they currently do not support negative indexes!

I'm not sure what this means in the context of Nim, but passing around a Rust references never does a copy (even into another thread).

(Disclaimer 2: it's not currently possible to pass a reference into another thread safely, but the standard library is designed to support it, the only missing piece is changing one piece of the type system, https://github.com/rust-lang/rfcs/pull/458 , to be able to guarantee safety.)