Can you please add some more relevant information to your comment? Expand upon why you feel it is similar to ADA, why ADA might be a better (or worse) alternative, if you have any experience working with ADA/Rust, etc. A three word comment does not add anything worthwhile to this thread. If you're on HN and commenting, please refrain from throwing whispers of thoughts down as they come to you, and instead take the opportunity to reply with something meaningful.
I have no real experience, just college classes in ADA. And reading the rust documentation reminded me of ADA. I can't hardly explain more than that is an old feeling I've only had when I studied ADA.
I wasn't sarcastic or trolling, but I understand it's hard to know with a cryptic 3 words sentence.
ps: I gathered some thoughts. It reminded me of ADA because it's designed to be low-level, yet embed high-level concepts and typing (generics).
I have real experience with ADA (also C, C++ and many others), and I have discovered that ADA is brilliant, a way underestimated language. But ADA requires a lot of discipline which is a possible reason why many developers don't like it.
I also like Rust. I haven't tested it yet (will try it) but the first impressions are good. But I think Rust will not be on par with ADA 2012 until it supports range values (like x : Integer Range 1..100) and contracts at least.
Asserts are good for the beginning but a language for really big software should have verification mechanisms which are implemented in SPARK (a subset of ADA).
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. :)
