4 ms·

I am learning Rust and SPARK2014, and I would think SPARK2014/Ada would be a better fit for high-integrity software for verifiable, embedded software than Rust.

by eggy 5y ago

I am learning Rust and SPARK2014, and I would think SPARK2014/Ada would be a better fit for high-integrity software for verifiable, embedded software than Rust. This was the older article that stimulated me to look at Ada and then SPARK2014 again: https://www.embedded.com/spark-2014-why-i-am-backing-a-predictable-winner/ https://www.embedded.com/spark-2014-why-i-am-backing-a-predi... EDIT: Cool list of SPARK2014/Ada embedded projects: https://blog.adacore.com/tag/embedded%20development https://blog.adacore.com/tag/embedded%20development

nicoburns 5y ago
That's probably true for now. But only because there's no equivalent to SPARK for Rust yet. Rust + something like SPARK could be really amazing.
- gavinray 5y ago
  There are some things that attempt to come close. Prusti by ETH Zurich is maybe the closest. https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev https://www.pm.inf.ethz.ch/research/prusti.html https://www.pm.inf.ethz.ch/research/prusti.html extern crate prusti_contracts; use prusti_contracts::*; #[requires(something)] #[ensures(result >= a && result >= b)] #[ensures(result == a || result == b)] fn max(a: i32, b: i32) -> i32 { if a > b { a } else { b } } Ada seems like a fantastic language though, and the 202x edition brought some niceties to the language.
  - eggy 5y ago
    I am an Ada/SPARK novice, but on first look Prusti seems to deal with contracts, but I am not sure how much more of the Ada/SPARK system it may covergg. I used to dislike Ada and SPARK due to their verbosity, but after studying some of the embedded work in them, and what they bring to the table, I am no longer put off by that or syntax. I've seen Julia and even Elixir projects in areas that would better suit Ada/SPARK, but I think it is due to their popularity rather than applicability. But things like Elixir's Nerves platform is very interesting in bringing the BEAM to the embedded world, and I love Pluto notebooks for Julia, but for high-integrity software I think I'll try and leverage Ada/SPARK's capabilities and pedigree for now. I will look further into Prusti this weekend.
- Jtsummers 5y ago
  Rust's type system still lacks the expressivity of Ada. Rust has a lot to teach Ada (and you see this coming out from AdaCore's blog recently with efforts to add lifetime analysis to SPARK), but Rust has a ton to learn from Ada as well.
- philzook 5y ago
  Interesting work in that direction https://www.youtube.com/playlist?list=PL-uEDsw-7yRLYMEdlvh4udnjK3JtGJgSh https://www.youtube.com/playlist?list=PL-uEDsw-7yRLYMEdlvh4u... Rust verification Workshop 2021
- eggy 5y ago
  I agree, but I just turned 57 (been programming since 1978 for fun), and there is so much already done in Ada that powers SPARK that it will be a while for it to be tried and true. Although, with all the work on theorem provers and such, maybe it will be exponential and I'll be around to see it. I really like Zig too, but I am staying with Rust because of its inertia. At heart, I love J/APL, but I use them for wholly different reasons.
nix23 5y ago
Ada is absolutely great, it's a shame that is was "closed" behind really expensive compilers and government work in the past. GNAT Aux could use some help too: http://www.dragonlace.net/ http://www.dragonlace.net/

by eggy 5y ago

nicoburns 5y ago

That's probably true for now. But only because there's no equivalent to SPARK for Rust yet. Rust + something like SPARK could be really amazing.

gavinray 5y ago
There are some things that attempt to come close. Prusti by ETH Zurich is maybe the closest. https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev https://www.pm.inf.ethz.ch/research/prusti.html https://www.pm.inf.ethz.ch/research/prusti.html extern crate prusti_contracts; use prusti_contracts::*; #[requires(something)] #[ensures(result >= a && result >= b)] #[ensures(result == a || result == b)] fn max(a: i32, b: i32) -> i32 { if a > b { a } else { b } } Ada seems like a fantastic language though, and the 202x edition brought some niceties to the language.
- eggy 5y ago
  I am an Ada/SPARK novice, but on first look Prusti seems to deal with contracts, but I am not sure how much more of the Ada/SPARK system it may covergg. I used to dislike Ada and SPARK due to their verbosity, but after studying some of the embedded work in them, and what they bring to the table, I am no longer put off by that or syntax. I've seen Julia and even Elixir projects in areas that would better suit Ada/SPARK, but I think it is due to their popularity rather than applicability. But things like Elixir's Nerves platform is very interesting in bringing the BEAM to the embedded world, and I love Pluto notebooks for Julia, but for high-integrity software I think I'll try and leverage Ada/SPARK's capabilities and pedigree for now. I will look further into Prusti this weekend.
Jtsummers 5y ago
Rust's type system still lacks the expressivity of Ada. Rust has a lot to teach Ada (and you see this coming out from AdaCore's blog recently with efforts to add lifetime analysis to SPARK), but Rust has a ton to learn from Ada as well.
philzook 5y ago
Interesting work in that direction https://www.youtube.com/playlist?list=PL-uEDsw-7yRLYMEdlvh4udnjK3JtGJgSh https://www.youtube.com/playlist?list=PL-uEDsw-7yRLYMEdlvh4u... Rust verification Workshop 2021
eggy 5y ago
I agree, but I just turned 57 (been programming since 1978 for fun), and there is so much already done in Ada that powers SPARK that it will be a while for it to be tried and true. Although, with all the work on theorem provers and such, maybe it will be exponential and I'll be around to see it. I really like Zig too, but I am staying with Rust because of its inertia. At heart, I love J/APL, but I use them for wholly different reasons.

nix23 5y ago

Ada is absolutely great, it's a shame that is was "closed" behind really expensive compilers and government work in the past. GNAT Aux could use some help too: http://www.dragonlace.net/ http://www.dragonlace.net/