Using SPARK to Prove 255-Bit Integer Arithmetic from Curve25519 | Hacker News Reader

Using SPARK to Prove 255-Bit Integer Arithmetic from Curve25519

blog.adacore.com

54 pointsbased210 comments

Just started reading/working through the book, "Building High Integrity Applications with Spark". I started with assembler, then basic and c, and took Turbo Pascal in the late 80s. I am very interested in safer, secure programming, and Spark and Rust seem to be approaching the hub from different spokes of the same wheel. I was playing with F/F# toolchain, but F is a bit formal for me, or at least not very clear for me.

The use of Spark on embedded devices, and CubeSats has sparked my interest ;)

I found the code and explanation in the article easy to follow although the subject matter is not in my domain.

I used to work in SPARK (all caps), and while I don't miss the industry, I do miss working with the language.

When you use it as it was meant to be used, it's incredibly empowering, it's like working with the world's most observant pair programmer.

The book remains one of the best books I've read on software development, although obviously it's from a very specific view.

Thanks for pointing out it's SPARK (all caps). I usually never miss this even on previous SPARK post I've made on HN. I was looking into Apache Spark recently, and it must have crossed lobes!

I am finding it to be really cool, and the verbosity isn't bothering me like it does in other languages.

I also picked up "Analysable Real-Time Systems Programmed in Ada" just for the RT aspects, and I am wondering how what I read and learn in this book can be leveraged by my push into SPARK. I am mainly looking to write controls software for the industry I work in Entertainment engineering, where performer flying winches, and all sorts of show action equipment have made the transition from neat, bespoke machines, to a regulated industry with standards like all other fields of engineering.

If you don't mind, what industry were you working in, and why don't you miss it? Have you been able to use SPARK at all in your current industry? Thanks!

Sorry for the slow reply.

I used to work for Praxis (now part of Altran) who used to be the owners of the SPARK tech, in fact I spent a while working in the SPARK team on the automated theorem prover technology.

Howerver this was a consultancy working in the aerospace and defense industry, and it frequently working away from home at the client's sites, on frequently very poorly run projects. I loved the technology, but I found the way things got done frustrating.

Building software in SPARK for stage equipment sounds like a good fit. I'd be very interested to hear how you get on.

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.

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.

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_th...

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!

The title should be corrected to "SPARK", not "Spark". It's used all caps each time it's mentioned on the page. That's also how I've seen this tool referred to elsewhere in the programming language literature: https://en.wikipedia.org/wiki/SPARK_(programming_language)

Yeah, seconded, i thought this was about running large-int arithmetic on apache spark.

Corrected now. This is an unfortunate wave-particle when it comes to casing, which HN's software tries to autocorrect in titles.

Reply on news.ycombinator.com