7 ms·

I still play with Rust (and Zig), but I have decided to put my work efforts into SPARK[1], the subset of Ada, for high-integrity software and formal verificatio

by eggy 4y ago

I still play with Rust (and Zig), but I have decided to put my work efforts into SPARK[1], the subset of Ada, for high-integrity software and formal verification. I know AdaCore and Ferrous Systems are collaborating in trying to bring a lot of Ada/Spark's capabilities to Rust, but this is still going to be some time. Ada has a longer legacy in this game. I am working on safety critical control systems and there is a lot to prune from existing work in this area in SPARK and Ada. This book[2], "Building High Integrity Applications with SPARK" really sold me on the benefits. It is a great intro of how SPARK was used for the CubeSat program at Vermont Technical College (VTC). A CubeSat was successfully launched in 2013. I could not find any critical mission software written in Rust yet especially that far back. I found Julia's selection for a flight collision avoidance system perplexing[3], but it proves a PLs syntax and evangelism (maybe not in this case), can bias a selection of a PL for such tasks. People find Ada/SPARK's syntax and methods verbose and similar to Pascal or other PLs, however, I was up and running quickly in it as opposed to Rust. You can program to bare metal in SPARK, and the tools are already there to provide high-integrity software. The tools for SPARK automate most of the verification. Most of Rust's wishlist is already in SPARK (and Ada). I hope the Ferrous Systems and AdaCore collab bears fruit for Rust, but I have been programming since 1978, and I play with many PLs, but I found Rust's initial learning curve very off putting and I don't have the time to wait for it to mature to SPARK's level. And this is from someone who loves J/APL/BQN and Lisp, so I have no issue with different programming paradigms. I found Zig much easier to get things done from the start, although it does not strive to be a SPARK or Rust. [1] https://www.adacore.com/sparkpro https://www.adacore.com/sparkpro [2] https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736 https://www.amazon.com/Building-High-Integrity-Applications-... [3] https://juliahub.com/case-studies/lincoln-labs/ https://juliahub.com/case-studies/lincoln-labs/

pjmlp 4y ago
NVidia also went through a similar decision for their high security critical firmware.
celurian92 4y ago
what resources can you suggest to learn formal verification and implement it to make high integrity fault tolerant services? I am quite intrigued by AdaCore. Want to try it out. I dont know much about Formal Verification.
- thesuperbigfrog 4y ago
  https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification AdaCore SPARK Introduction: https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html https://www.synopsys.com/verification/static-and-formal-verification/formal-book.html https://www.synopsys.com/verification/static-and-formal-veri...
brianzelip 4y ago
Here’s a recent podcast episode that looks at Rust and Ada with some folks who work on Ada Core, https://rustacean-station.org/episode/067-quentin-ochem-florian-gilcher/ https://rustacean-station.org/episode/067-quentin-ochem-flor...
galangalalgol 4y ago
People have picked stranger things than julia for safety critical control systems. I know people have generated it from simulink and have used labview, and it wouldn't surprise me if somewhere someone is using an excel macro to control the pressure system on a boiler... The world is a scary place. Reading theough the spark tutorials and examples seems fairly similar to the rustlings excercise. I find the ways spark prevents problems, like forbidding side effects, is more onerous than the borrow checker making me specify a lifetime every so often. I'm not saying you are wrong to prefer spark, just that people with different backgrounds will find the learning curves different. You have been programming longer than I've been alive, so you certainly have a different perspective. I started with c64 basic then c on the amiga 500, then x86 assembler on 386, them turbo pascal, then turbo c++ on the 386. I can't argue that spark isn't more mature for formal verification, but it feels like formal verification relies heavily on correct contract specifications with no way to measure when your contracts are correct. Unit tests and coverage at least give me a little feel good that I wrote enough tests for my rust.
- ngrilly 4y ago
  I started working with functional safety only two years ago, and I've been surprised when colleagues expressed that Simulink was actually the go-to solution for functional safety software where they were working before. The logic being that the Simulink toolchain is qualified for functional safety, and if you use it in combination with a qualified C toolchain and RTOS, then you're good to go, certification-wise.
  - jfmc 4y ago
    My impression when working with people using Simulink is that 'safety' is much weaker that for people working on formal methods, and certification limited a lot the kind of programs that they would write. It made totally sense for their domain, but -- as a general practice to write software -- it didn't impress me at all. I may be wrong.
    - ngrilly 4y ago
      I was expecting functional safety standards to require the use of formal methods, similar for example to how AWS uses TLA+, but I was surprised to discover it was not a requirement at all.
thesuperbigfrog 4y ago
More about Ferrocene, the safety-critical Rust toolchain / specification that is in the works: https://www.adacore.com/ferrocene https://www.adacore.com/ferrocene https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ https://spec.ferrocene.dev/ https://spec.ferrocene.dev/
bobajeff 4y ago
I've looked a tiny bit into Ada and I like the language. I particularly like the pascal-like syntax and the ranges feature. However I love rusts cargo and build system better than Alire. As Alire seems to bolted ontop of gprbuild. I also find it unfun to go back to forward declaration and definition (ads) files. It also seems to me the rust ecosystem has more libraries in things I'm interested in and better support for the platforms I'm interested in.
- eggy 4y ago
  What libraries are you interested in that Rust has and other PLs do not? What is your main use of Rust? It all depends on what you are doing. I use Zig for fun game dev stuff, and not SPARK, but for the safety-critical control systems, it's SPARK, not Zig or Rust.
  - bobajeff 4y ago
    I'm using rust to develop a internet client. So I need libraries for gui; rust has many to choose from (I'm using gtk currently). I see a few that plan on supporting Android which I'd like to port to down the line. Of course rust has many networking libraries also so I feel covered there. Safety is fairly important and I like ada/spark for that but rust's community seems to be farther along in terms of support for Android and looks way more active right now.
shakow 4y ago
> I found Julia's selection for a flight collision avoidance system perplexing From [3]: > Julia is [...] executable Indeed, that's a useful feature for a programming language :)
micronian2 4y ago
Hi, Regarding the collaboration between AdaCore and Ferrocene, the effort is to produce a Rust toolset that is qualified for safety critical usage (e.g. verification of object code that is produced, etc). That is _not_ the same as bringing SPARK-like language capabilities to Rust. I think too many people get that confused.

by eggy 4y ago

pjmlp 4y ago

NVidia also went through a similar decision for their high security critical firmware.

celurian92 4y ago

what resources can you suggest to learn formal verification and implement it to make high integrity fault tolerant services? I am quite intrigued by AdaCore. Want to try it out. I dont know much about Formal Verification.

thesuperbigfrog 4y ago
https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification AdaCore SPARK Introduction: https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html https://www.synopsys.com/verification/static-and-formal-verification/formal-book.html https://www.synopsys.com/verification/static-and-formal-veri...

brianzelip 4y ago

Here’s a recent podcast episode that looks at Rust and Ada with some folks who work on Ada Core, https://rustacean-station.org/episode/067-quentin-ochem-florian-gilcher/ https://rustacean-station.org/episode/067-quentin-ochem-flor...

galangalalgol 4y ago

People have picked stranger things than julia for safety critical control systems. I know people have generated it from simulink and have used labview, and it wouldn't surprise me if somewhere someone is using an excel macro to control the pressure system on a boiler... The world is a scary place. Reading theough the spark tutorials and examples seems fairly similar to the rustlings excercise. I find the ways spark prevents problems, like forbidding side effects, is more onerous than the borrow checker making me specify a lifetime every so often. I'm not saying you are wrong to prefer spark, just that people with different backgrounds will find the learning curves different. You have been programming longer than I've been alive, so you certainly have a different perspective. I started with c64 basic then c on the amiga 500, then x86 assembler on 386, them turbo pascal, then turbo c++ on the 386. I can't argue that spark isn't more mature for formal verification, but it feels like formal verification relies heavily on correct contract specifications with no way to measure when your contracts are correct. Unit tests and coverage at least give me a little feel good that I wrote enough tests for my rust.

ngrilly 4y ago
I started working with functional safety only two years ago, and I've been surprised when colleagues expressed that Simulink was actually the go-to solution for functional safety software where they were working before. The logic being that the Simulink toolchain is qualified for functional safety, and if you use it in combination with a qualified C toolchain and RTOS, then you're good to go, certification-wise.
- jfmc 4y ago
  My impression when working with people using Simulink is that 'safety' is much weaker that for people working on formal methods, and certification limited a lot the kind of programs that they would write. It made totally sense for their domain, but -- as a general practice to write software -- it didn't impress me at all. I may be wrong.
  - ngrilly 4y ago
    I was expecting functional safety standards to require the use of formal methods, similar for example to how AWS uses TLA+, but I was surprised to discover it was not a requirement at all.

thesuperbigfrog 4y ago

More about Ferrocene, the safety-critical Rust toolchain / specification that is in the works: https://www.adacore.com/ferrocene https://www.adacore.com/ferrocene https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ https://spec.ferrocene.dev/ https://spec.ferrocene.dev/

bobajeff 4y ago

I've looked a tiny bit into Ada and I like the language. I particularly like the pascal-like syntax and the ranges feature. However I love rusts cargo and build system better than Alire. As Alire seems to bolted ontop of gprbuild. I also find it unfun to go back to forward declaration and definition (ads) files. It also seems to me the rust ecosystem has more libraries in things I'm interested in and better support for the platforms I'm interested in.

eggy 4y ago
What libraries are you interested in that Rust has and other PLs do not? What is your main use of Rust? It all depends on what you are doing. I use Zig for fun game dev stuff, and not SPARK, but for the safety-critical control systems, it's SPARK, not Zig or Rust.
- bobajeff 4y ago
  I'm using rust to develop a internet client. So I need libraries for gui; rust has many to choose from (I'm using gtk currently). I see a few that plan on supporting Android which I'd like to port to down the line. Of course rust has many networking libraries also so I feel covered there. Safety is fairly important and I like ada/spark for that but rust's community seems to be farther along in terms of support for Android and looks way more active right now.

shakow 4y ago

> I found Julia's selection for a flight collision avoidance system perplexing From [3]: > Julia is [...] executable Indeed, that's a useful feature for a programming language :)

micronian2 4y ago

Hi, Regarding the collaboration between AdaCore and Ferrocene, the effort is to produce a Rust toolset that is qualified for safety critical usage (e.g. verification of object code that is produced, etc). That is _not_ the same as bringing SPARK-like language capabilities to Rust. I think too many people get that confused.