Hacker News Reader

Comment by Yoric | Hacker News Reader

For what it's worth, many Rust developers (including myself) are also Ada fans.

Note that ranged types, decimal types, etc. can fairly easily be emulated in Rust, with what I find is a clearer error mechanism.

SPARK is, of course, extremely cool :) There are several ways to work with theorem provers and/or model checkers in Rust, but nothing as nicely integrated as SPARK so far.

View on HN

I would quibble with the "fairly easily" part. It will likely become possible to make them as ergonomic as the Ada variety if Rust's const generic and constant evaluation facilities are extended far enough, but this would also open up the can of worms of essentially giving Rust the full capabilities of a dependently-typed language (at least in its compile-time subset), which Rust's dev community may not necessarily be OK with.

I'll grant you that Rust is not nearly as ergonomic as Ada in this domain, but doing it manually is fairly easy. Turning it into a library is a bit more complicated - these days, I'd do it with macros. Of course, making sure that the compiler knows about it for optimization purposes would require lots of const generic.

The real benefit of Adas typing is that it is so easy to utilise often preventing logic errors.

And this is definitely a strong benefit.

The benefit of Rust's typing is that (in the absence of `unsafe` or bugs in the compiler or stdlib), it's a simple theorem prover. Much less powerful than the theorem provers you can use with SPARK, but it's a start :)

Reply on news.ycombinator.com