The way I understand them (and I say this a lot, but I could be wrong) is that it's like a more powerful version of Eiffel's design by contract, which allows the compiler to test whether invariants hold at compile time rather than just throwing assertions at runtime.
Another option (addon) would be to use commented invariants like in SPARK which are tested against the code by an automatic verification system even before compile time. To get an impression what it means, please read:
Interesting. Not sure precisely what you mean by "bounded memory usage", but if you mean array bounds checking then you're correct in that Rust requires a runtime component for that.
no, I mean that in SPARK you are able to state that some program will not grow it's memory usage indefinitely (I believe you also have worst case time analysis).
AFAICT this requires forbidding recursion, unbounded loops and use of heap allocators or types/procedures which in turn have access to such facilities.
Or somewhat equivalently: the SPARK subset of Ada is statically verifiable by not being turing complete, so bits of the code can be verified, and elsewhere the full Ada language can be used.
I am not sure if Rust can emulate this.
(Again, I am not an Ada/SPARK developer so all of what I wrote may be wrong, do not take life decisions based on what I write)
Thanks for the clarification. I can't find the source, but I believe there's a quote somewhere from Graydon (Rust's head designer) stating that complete static verifiability isn't a goal they're aiming for, at least not for the foreseeable future. However, I suppose that doesn't preclude someone else from forking the Rust compiler and devising a non-Turing-complete subset on their own. :)
http://doc.rust-lang.org/doc/rust.html#typestate-system
The way I understand them (and I say this a lot, but I could be wrong) is that it's like a more powerful version of Eiffel's design by contract, which allows the compiler to test whether invariants hold at compile time rather than just throwing assertions at runtime.