3 ms·

Has anyone developed in SPARK [0]? My understanding, its significantly safer than Rust (and based on Ada) with equal performance. A comparison chart of Ada vs

Has anyone developed in SPARK [0]? My understanding, its significantly safer than Rust (and based on Ada) with equal performance. A comparison chart of Ada vs Rust vs SPARK [1]. Most notable: Rust mainly provides memory safety ... but SPARK provides not just memory safety, but also safety from all run-time errors, formal properties, constraint checks, and more. [0] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) [1] https://blog.adacore.com/should-i-choose-ada-spark-or-rust-over-c-c https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...

Ygg2 2y ago
> My understanding, its significantly safer than Rust (and based on Ada) with equal performance. Ada or Ada Spark? Ada Spark is more of a theorem prover, so the comparison to Rust is a bit weird. It's true it's safer - it will protect you from a more programming errors, but you need more annotations to prove properties of a program.
ajxs 2y ago
I'd never seen [1] before. Thanks for the link! That's a great and even-handed discussion of the topic. I've written a lot of hobby Ada code. I really like the language. Recently I did some research into how memory safety in Ada/SPARK compares with Rust[0]. My conclusion was that Rust is better at outright preventing common memory-related errors, but Ada has a lot of great features which let you avoid them in the first place. SPARK is a bit intimidating, but you can pretty much achieve parity with Rust on memory safety, and achieve a higher degree of safety overall. I got a real kick out of someone's comment on Reddit saying 'Both Ada and Rust benefit from not being C'. 0: https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Against_Rust.html https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...
- tiffanyh 2y ago
  Amazing blog post, learned a lot. Thanks for writing & sharing it.

Ygg2 2y ago

> My understanding, its significantly safer than Rust (and based on Ada) with equal performance. Ada or Ada Spark? Ada Spark is more of a theorem prover, so the comparison to Rust is a bit weird. It's true it's safer - it will protect you from a more programming errors, but you need more annotations to prove properties of a program.

ajxs 2y ago

I'd never seen [1] before. Thanks for the link! That's a great and even-handed discussion of the topic. I've written a lot of hobby Ada code. I really like the language. Recently I did some research into how memory safety in Ada/SPARK compares with Rust[0]. My conclusion was that Rust is better at outright preventing common memory-related errors, but Ada has a lot of great features which let you avoid them in the first place. SPARK is a bit intimidating, but you can pretty much achieve parity with Rust on memory safety, and achieve a higher degree of safety overall. I got a real kick out of someone's comment on Reddit saying 'Both Ada and Rust benefit from not being C'. 0: https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Against_Rust.html https://ajxs.me/blog/How_Does_Adas_Memory_Safety_Compare_Aga...

tiffanyh 2y ago
Amazing blog post, learned a lot. Thanks for writing & sharing it.