Hacker News Reader

Comment by bitcracker | Hacker News Reader

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).

View on HN

You should take a look at Rust's typestate mechanism:

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.

I may be wrong, but I believe SPARK may have greater validation fecilities than what rust provides at the moment.

E.g. SPARK allows static verification of bounded memory usage, which I am not sure if rust's `check` is able to express.

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. :)

Interesting! I am curious how it develops.

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:

http://www.adacore.com/home/products/sparkpro/tokeneer/disco...

Reply on news.ycombinator.com