3 ms·

Rust and SPARK are totally different things. SPARK was designed to build high integrity applications, Rust was designed to build applications that don't crash b

by blub 7y ago

Rust and SPARK are totally different things. SPARK was designed to build high integrity applications, Rust was designed to build applications that don't crash because of invalid memory accesses. The second is a much, much weaker guarantee, basically any language used nowadays besides C and C++ will offer the same memory safety guarantee as Rust.

touisteur 7y ago
The SPARK teams at AdaCore & Altran UK are working hard right now to bring proved memory safety, some kind of borrow-checker to SPARK (and then hopefully, Ada). I think they have something working already but they want it to work in an industrial, high integrity context, so : for every case, all the time, with minimum training and complexity for the developer. Amazing what a small team of clever, focused people can achieve. By the way, it's great that Rust is starting to get 'formal-proof' interest, but I fear they're starting on a path without looking at the experience of others. I'm thinking about creating an adhoc language to write properties, pre-/post- conditions, etc. The power of SPARK2014 is in big part the result of Ada2012 integrating executable contracts /written directly in Ada/. This enables so much ! Lower learning curve, the ability to transition smoothly from Ada to SPARK bronze (every variable is always initialized before use, no aliasing...), silver (absence of runtime errors and since Ada comes with tons or runtime checks, that's amazingly safe already), gold (prove some Properties, kind of the PBT of proof :-) ), platinum (full specification, proved) levels... At the very least, now you have contrats in Ada, you can improve your interfaces. Where typing wasn't enough to express semantics, contacts can help. If you've written properties/contracts, now you can verify them with SPARK or if too hard, test it, fuzz it... I also hope they'll look into why3 and all the amazing work that's been done to help abstract over SMT solvers, and allow to play on each solver's strength ! Alt-ergo, cvc4, z3... It would be great for all 'safe' languages (SPARK2014, Frama-C, Java/JML, now rust) to share some common good base layers for proof. I know there's a lot of collaboration and cross-pollination between the Frama-C and SPARK2014 worlds.
eggy 7y ago
Sure they are different: OOP/Pascal-like vs. multi-paradigm/C-like language, etc., but the point of the spoke and hub analogy is that coming from different sides (spokes), but directing towards something like safe, secure programming is what they have in common (the hub), and has instigated the ADA/SPARK community to take notice, and vice versa for Rust. Look at these two discussions for a bit of where I am going with it: https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_the_best_thing_that_could_have/ https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_th... https://www.reddit.com/r/rust/comments/7ibea3/safe_pointers_in_spark_ada_inspired_by_rusts/ https://www.reddit.com/r/rust/comments/7ibea3/safe_pointers_... I like Rust (and I like Zig too). I like ADA/SPARK 2014. I am currently interested in safe, secure, verifiable and validated software development, and these PLs are on my radar. I have also considered a duo of F*/F#, but they are not ticking as many boxes as ADA/SPARK 2014. I'd love to see the cross pollination or competition between Rust and SPARK 2014 lead to them both improving, and borrowing concepts from each other. Rust is being touted more and more for embedded, and SPARK 2014 is already there. Now if I could get SPARK/Rust in a Lisp!

by blub 7y ago

touisteur 7y ago

The SPARK teams at AdaCore & Altran UK are working hard right now to bring proved memory safety, some kind of borrow-checker to SPARK (and then hopefully, Ada). I think they have something working already but they want it to work in an industrial, high integrity context, so : for every case, all the time, with minimum training and complexity for the developer. Amazing what a small team of clever, focused people can achieve. By the way, it's great that Rust is starting to get 'formal-proof' interest, but I fear they're starting on a path without looking at the experience of others. I'm thinking about creating an adhoc language to write properties, pre-/post- conditions, etc. The power of SPARK2014 is in big part the result of Ada2012 integrating executable contracts /written directly in Ada/. This enables so much ! Lower learning curve, the ability to transition smoothly from Ada to SPARK bronze (every variable is always initialized before use, no aliasing...), silver (absence of runtime errors and since Ada comes with tons or runtime checks, that's amazingly safe already), gold (prove some Properties, kind of the PBT of proof :-) ), platinum (full specification, proved) levels... At the very least, now you have contrats in Ada, you can improve your interfaces. Where typing wasn't enough to express semantics, contacts can help. If you've written properties/contracts, now you can verify them with SPARK or if too hard, test it, fuzz it... I also hope they'll look into why3 and all the amazing work that's been done to help abstract over SMT solvers, and allow to play on each solver's strength ! Alt-ergo, cvc4, z3... It would be great for all 'safe' languages (SPARK2014, Frama-C, Java/JML, now rust) to share some common good base layers for proof. I know there's a lot of collaboration and cross-pollination between the Frama-C and SPARK2014 worlds.

eggy 7y ago

Sure they are different: OOP/Pascal-like vs. multi-paradigm/C-like language, etc., but the point of the spoke and hub analogy is that coming from different sides (spokes), but directing towards something like safe, secure programming is what they have in common (the hub), and has instigated the ADA/SPARK community to take notice, and vice versa for Rust. Look at these two discussions for a bit of where I am going with it: https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_the_best_thing_that_could_have/ https://www.reddit.com/r/ada/comments/7wzrqi/why_rust_was_th... https://www.reddit.com/r/rust/comments/7ibea3/safe_pointers_in_spark_ada_inspired_by_rusts/ https://www.reddit.com/r/rust/comments/7ibea3/safe_pointers_... I like Rust (and I like Zig too). I like ADA/SPARK 2014. I am currently interested in safe, secure, verifiable and validated software development, and these PLs are on my radar. I have also considered a duo of F*/F#, but they are not ticking as many boxes as ADA/SPARK 2014. I'd love to see the cross pollination or competition between Rust and SPARK 2014 lead to them both improving, and borrowing concepts from each other. Rust is being touted more and more for embedded, and SPARK 2014 is already there. Now if I could get SPARK/Rust in a Lisp!