Re:Ada's Dependent Types, and Its Types as a Whole
by Yoric on Saturday December 28, 2024 @12:44PM
(#42532766)
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.
[ Parent
| on HN ]
Re:Ada's Dependent Types, and Its Types as a Whole
by kevlar700 on Saturday December 28, 2024 @06:46PM
(#42535961)
The real benefit of Adas typing is that it is so easy to utilise often preventing logic errors.
Re:Ada's Dependent Types, and Its Types as a Whole
by Yoric on Saturday December 28, 2024 @07:41PM
(#42536299)
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 :)