Can someone point me to an explanation of "Nim is the only language that leverages automated proof technology to perform a disjoint check for your parallel code"? This is mentioned prominently on the main page...but scanning the docs, the FAQ, Dr. Dobbs, and Googling 'nim disjoint' didnt lead me to a detailed explanation.
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.
> 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.
> 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.)
Well, it will be hard to find a proof for it being the "only" language to do so, since as one of the commenters mentioned there is indeed at least one other. But http://nim-lang.org/manual.html#parallel-spawn seems to discuss it a bit. Or did you want more details? If so, what kind? Actually I don't know anything about Nim anyway, so whatever your question is I can't answer it.
Well I did my homework. When you find another language that does it in a somewhat similar fashion, I'll happily change the website. ;-) I didn't think Rust counts, but since it's constantly changing, I will have a fresh look at it.
It doesn't seem like an accurate claim, as Rust also has the ability to reason about uniqueness of data. Rust uses a type system to do it—which, via Curry-Howard, qualifies as "automated proof technology" :)
It looks like Nim has some ability to reason about arithmetic identities natively, which is neat. In practice Rust uses iterators to encode the same sorts of common patterns in the type system.
