This is definitely the article I’ve been waiting for at least on the SPARK side. I was shocked when author said he worked at AdaCore. He was way more fair to Rust than I expected even throwing AdaCore under the bus in the section on their GPL and community handling. They deserved it but I thought it would be an outsider doing it. End result is similar to what I came up with: SPARK wins on anything static or verified w/ Rust winning on dynamic or flexible concurrency; SPARK wins on predictability with Rust on productivity. Now, author needs to do a detailed comparison between Rust and Ada 2012 which is its actual competition.
That good stuff said, author was way off on the historical aspect. Should be corrected.
“Rust is probably the most notable indication of the growing need for languages with safety in mind.”
The forced introduction of GC’d languages for apps by Sun and Microsoft were the indication. A need for safety is strongly established. Rust is first push that’s popular to do safety with no GC.
“while Rust was being developed, another effort was undertaken by a different community, also trying to raise the bar in terms of safety.”
Maybe he’s just trying to be impartial. One of inventors of software engineering, Dijkstra, was using formal specs with code on his OS in 1960’s. CompSci, Defense, hardware industry, and some in safety-critical were all building or using tools for formally-verified systems for decades. Most of industry and FOSS ignored it. British researchers defined SPARK in 1988 with it spun off to Praxis Limited for industrial use. This effort actually reduced amount of safety and verification vs full, formal verification with aim to automate as much as possible at code level for increased adoption by non-experts in formal methods. After many iterations and a partnership with AdaCore, the tool eventually achieved its goal on tech side with an open-source version, too. Another effort at similar time with similar aims on specification side was Eiffel method.
On Rust side, I don’t have the big picture. I do know their core capability, the memory safety, came from Greg Morrisett’s work on Cyclone language that modified C to be safer. Greg was an expert in type theory and language-level security with enough overlap to tie him into high-assurance field. He also worked on extending ML’s. Graydon wanted a safe, fast language. He combined unique capabilities he saw in Cyclone with features from other languages or paradigms. He likewise wrote the compiler in an ML (Ocaml) for fast, reliable development. He was sponsored by Mozilla with teams focused on the tech and strong community (AdaCore’s failure). The rest is history.
Long story short: the forces behind both SPARK and Rust have always been there. Just ignored. Roughly three, smart people paying attention to it and building on it was all it took to get the two languages started. Imagine what would happen if more people did this. That is, more CompSci people tried to be practical (in FOSS not patents!) or more developers building on strongest stuff from CompSci. Anyway, both have work underway to specify them for later full, formal verification with SPARK being added to CompCert compiler. Both are usable now for robust apps. If you do safety or security, you should be defaulting on them unless good reason otherwise.
Note: The Archive.org page for Morrisett’s old site at Harvard showed his publication in 2006 was first time it got many users. Then, it was pretty small until 2016. I attribute that to Rust mentioning Cyclone was one of its influences. It’s a good illustration, though, of what I talk about here of tech in high-assurance security or systems… often CompSci itself… taking 10+ years to reach mainstream. Gotta smash that barrier somehow. I do what I can sharing links but “I am but one man.”
EDIT: Dude is apparently funny too.
FWIW, when I saw the title of this post, I was really surprised that it was submitted by someone other than you. :)
Thanks for noticing haha. Yeah, Id definitely have submitted it if I saw it first. Glad others are keeping eye out for such things. Also, glad an AdaCore employee is studying Rust. I really want them to port its temporal safety to Ada/SPARK. With that, it’s number 1 hands down.
Hey Nick, you really should consider opening a blog or at least collect this kind of comments somewhere!
Your comment made me look up SPARK. :D Thank you.
Very welcome! :) You might also like seeing how the inventor applies it given they’re one of few companies that engineer software:
And heres one showing how Ada was designed to systematically eliminate programmer error. It’s a book but easy to skim thanks to organization.
This is the best article I have seen comparing Rust to some other languages.
I don’t quite understand what safe means in the context of this article. Rust guarantees memory errors don’t exist, but this doesn’t guarantee my software is safe from bugs, safe from hackers or safe from some other catastrophe.
There’s a few definitions depending on who you ask. The commonality is safe from low-level errors that cause crashes or hacks. Ada is certainly safe from a lot of those. Rust is safe from a few including one Ada didn’t pull off. SPARK code is provably safe from a pile of them.