undefined | Better HN

0 pointszozbot2341y ago0 comments

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.

0 comments

Yoric1y ago

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.

kevlar7001y ago

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

Yoric1y ago

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

j / k navigate · click thread line to collapse

0 pointszozbot2341y ago0 comments

0 comments

Yoric1y ago

kevlar7001y ago

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

Yoric1y ago

And this is definitely a strong benefit.

j / k navigate · click thread line to collapse