I have been attempting to compare Ada and Rust for a while, but never got around to doing it quite so much in depth.
So, my take on this is that:
- out of the box, Rust is distinctly better at memory safety than Ada without SPARK
- Ada + SPARK is extremely powerful (but iirc, SPARK doesn't allow compositional reasoning, which makes it harder to use in a crate-based library)
- for this specific use case, Rust's error model makes much more sense than Ada's (with or without SPARK)
- Ada's tooling to avoid memory allocation remain more powerful in some dimensions than Rust's.
Also, I think that we all (should) agree that the move towards memory safety in system-level programming is a very good thing, whether it comes through Rust, Ada, or any other language.
I have been attempting to compare Ada and Rust for a while, but never got around to doing it quite so much in depth.
So, my take on this is that:
- out of the box, Rust is distinctly better at memory safety than Ada without SPARK
- Ada + SPARK is extremely powerful (but iirc, SPARK doesn't allow compositional reasoning, which makes it harder to use in a crate-based library)
- for this specific use case, Rust's error model makes much more sense than Ada's (with or without SPARK)
- Ada's tooling to avoid memory allocation remain more powerful in some dimensions than Rust's.
Also, I think that we all (should) agree that the move towards memory safety in system-level programming is a very good thing, whether it comes through Rust, Ada, or any other language.