4 ms·

Rust and SPARK – Software Reliability for Everyone

3 points by nickpsecurity 10y ago

nickpsecurity 10y ago
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 by Meyers. 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. https://www.cs.cornell.edu/~jgm/jgm.html https://www.cs.cornell.edu/~jgm/jgm.html https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language) 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. https://www.quora.com/Why-is-Professor-Greg-Morrisett-so-fond-of-cows https://www.quora.com/Why-is-Professor-Greg-Morrisett-so-fon...
- kbenson 10y ago
  > 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. I think it might be less of "it just takes a long time" and more that it needs a champion, and that champion can't just have that one aspect, it needs to be attractive for other reasons. Rust is attractive for its safety, but not just for its safety. It also takes performance seriously. It also goes to great effort to provide convenience, where it doesn't interfere with safety. They did the same thing D or Nim did, but instead of just new and modern syntax and some garbage collected STDLIB stuff (which to be honest, you could just get out of a very comprehensive libc replacement), they added something you couldn't really do with a library, and you couldn't completely do with the same language semantics. So, it's not just a more modern and cleaner C/C++, it's also something you can't quite approximate in the C/C++ ecosystem, and that sets it apart.

3 points by nickpsecurity 10y ago

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 by Meyers. 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. https://www.cs.cornell.edu/~jgm/jgm.html https://www.cs.cornell.edu/~jgm/jgm.html https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language) 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. https://www.quora.com/Why-is-Professor-Greg-Morrisett-so-fond-of-cows https://www.quora.com/Why-is-Professor-Greg-Morrisett-so-fon...

kbenson 10y ago
> 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. I think it might be less of "it just takes a long time" and more that it needs a champion, and that champion can't just have that one aspect, it needs to be attractive for other reasons. Rust is attractive for its safety, but not just for its safety. It also takes performance seriously. It also goes to great effort to provide convenience, where it doesn't interfere with safety. They did the same thing D or Nim did, but instead of just new and modern syntax and some garbage collected STDLIB stuff (which to be honest, you could just get out of a very comprehensive libc replacement), they added something you couldn't really do with a library, and you couldn't completely do with the same language semantics. So, it's not just a more modern and cleaner C/C++, it's also something you can't quite approximate in the C/C++ ecosystem, and that sets it apart.