10 ms·
AdaCore and Ferrous Systems Joining Forces to Support Rust
- nix23 5y agoI have no connections to AdaCore, but the products are absolutely great (especially GNAT community edition).
- Argorak 5y agoI can share from Ferrous side that the partnership started "clicking" when we found our common interest in product quality and user service.
- touisteur 5y ago(paying) customer here. Support is quite something. gcc (C/Ada), tools, language questions or problems, you get some expert answering most often the same day, and you get experts chiming in, references to the Ada or GNAT reference manual or user manual, sometimes history, sometimes a 'meh you're right this isn't really satisfactory, let's see how we can improve'. I cherish the mails I got years ago from the late Robert Dewar watching the support tickets and joining in with compiler optimization patches some hours after being convinced of the usefulness of an idea. Woa. Even more impressive on the SPARK side, Yannick Moy, Claire Dross and Johannes Kanig are first rate minds. The libadalang effort is also a game changer for Ada and spark, really making legacy code analysis and refactoring, and overall tool building, so much easier. And the way they ramped up their fuzzing story once they realized the potential is quite something.
- the__alchemist 5y agoFerrous's embedded Rust tooling is outstanding. Ie its [Knurling App template](https://github.com/knurling-rs/app-template https://github.com/knurling-rs/app-template), and associated Probe-run, Deft, and flip-link. These make flashing and debugging Rust embedded very easy - easier than any embedded toolchain I've seen besides Arduino.
- listic 5y agoI wish HN supported markdown, at least the links.
- izietto 5y agoI don't, Markdown is good enough even as plain text to me
- Grimburger 5y ago[Check this cool similar new app out HN](http:/not.suspicious.com/nor/has/tracking)
- littlestymaar 5y agoBasic web browsing hygiene: hover links and see where they go before clicking on them. ULR shorteners aren't blocked on HN, despite being more dangerous than labeled links (because you have no way to know where they point to without clicking).
- pjmlp 5y agoThis are big news, congratulations to everyone making this happen! Looking forward to what it might bring into safer computing world.
- ajxs 5y agoThis is a very interesting move from AdaCore. I've been a vocal advocate of Ada as a general purpose programming language for a little while. I hope that this helps expose the language to a wider audience, and gives the wider programming community cause to reappraise Ada from a modern perspective. It's a language with a lot to offer.
- Argorak 5y agoI very much agree. Rust is often seen as C/C++-inspired, but I know a lot of the early team looked at Ada for inspiration. We have also seen in many evaluations of "new stacks" that we were invited in that Ada was evaluated along with Rust. The conclusion was often similar: both languages have matching ambitions, in different forms. Also, there's a ton of places where Ada is just "there" already, e.g. by having something like SPARK available and in production use for many years. I expressed some of those thoughts in the corresponding post on the Ferrous Systems blog: https://ferrous-systems.com/blog/ferrous-systems-adacore-joining-forces/ https://ferrous-systems.com/blog/ferrous-systems-adacore-joi...
- zppln 5y agoI'm curious as to what you see are the benefits of using Rust in high assurance applications, compared to the alternatives already available? In my experience (which doesn't include anything related to formal verification), when everything's said and done you're left with a fairly limited subset of your chosen language anyway.
- Argorak 5y agoRust makes quite a few things more rigorous (e.g. pairing allocations with deallocations and reference validity). It basically fulfills the job of a static analyzer baked into the language. It's also a vastly more analyzable language (in that its syntax is reasonably unambiguous and there's no dynamic runtime in play) and it can be integrated well. Toolchain quality (error reporting, built in testing, awareness of primitives like "libraries", etc.) is also a huge strong point. We're reasonably confident that we can use safe Rust as is, with strong guidance on how to do unsafe Rust. For a tangible investigation of that space, PolySync has a project that has a look at MISRA rules from a Rust perspective. https://github.com/PolySync/misra-rust/blob/master/MISRA-Rules.md#misrac https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul... Ada is a good example here: the language has not evolved something like MISRA-C (it has evolved SPARK for formal verification, but I see that differently).
- guerby 5y agoSoon a "pragma Import (Rust, MyFunction);" ? :)
- Argorak 5y agoLet's first get rustc qualified, but speaking on a high level, I believe Ada/Rust FFI has potential to make `unsafe`... safer. If someone wants to play around with this in the open, please don't hesitate to get in touch.
- xavxav 5y agoThis is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated. I'm curious what kinds of software they want to (eventually) verify, my PhD thesis is developing a verification tool for Rust (https://github.com/xldenis/creusot https://github.com/xldenis/creusot) and I'm always on the look out for case studies to push me forward. The road to formally verified Rust is still long but in my unbiased opinion looking quite bright, especially compared to other languages like C. Ownership typing really, really simplifies verification.
- bovermyer 5y agoVerifying software used to control rocket fueling systems sounds like a good idea to me.
- xavxav 5y agoThat kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.
- gameswithgo 5y agowhat are those tools written in?
- fgh 5y agoThis is a guess, but Simulink is most likely based on a mixture of C, C++ and Java (if we leave out MATLAB as an intermediate step).
- bluGill 5y agoIn large part because those models are easy to formally verify. I've become interested in SPARK of the past few years, but people tell me while you can verify it, it is hard to do right. (I have no idea) I don't work with them myself, but some of my coworkers do low level control of similar hardware and they mostly work in matlab for that reason. Well for new code, there is still a lot of C from 20+ years ago in production, it isn't formally verified but years of real world experience says it is pretty good. Everytime there is a new feature there is a decision to rewrite the whole in matlab, put in shims to write the new part in matlab, or just add the C.
- pabs3 5y agoIs Ferrocene going to be open source?
- eggy 5y agoI hope it follows the AdaCore model or a model that allows for similar industry customer support for the early adopters who put their businesses on the line. Is there a successful high-integrity software or safe software product out there to base this on? Just curious.
- steveklabnik 5y agoI don't know if the plans have changed, but originally: https://ferrous-systems.com/blog/sealed-rust-the-pitch/ https://ferrous-systems.com/blog/sealed-rust-the-pitch/ > This document will be maintained as an open source work, similar to other documentation components, though may be officially published as a standards document elsewhere. The validation tests demonstrating conformance to the specification would also be maintained in Open Source as a new collection of tests. EDIT: oh here's a better comment from Florian: https://www.reddit.com/r/rust/comments/sijixb/comment/hv9cpnu/?context=3 https://www.reddit.com/r/rust/comments/sijixb/comment/hv9cpn...
- brabel 5y agoCan we get a Rust version of Spark now? I think that would be really cool!
- eggy 5y agoI put Rust aside for now, but I like it. I am focusing on SPARK and Elixir/Nerves for now. I bought the book, "Building High Integrity Applications with SPARK", and followed along with the AdaCore resources, and it is amazing. Rust will not be there for a while, but this is exciting. I am happy to see goals being more important than choice of PL here. This article sort of put me over the edge to pursue SPARK [1]. For those who comment on verbosity or similarity to COBOL, I can say as an APL/J fan, and somebody who loves concise code with a mathy slant, SPARK is a great way to create high-integrity software with tooling along the whole development chain. I will be working on a controls system, and Rust is just not there yet to commit to it, but I will certainly keep my eye on this great team up between AdaCore and Ferrous Systems! [1] https://blog.adacore.com/how-to-prevent-drone-crashes-using-spark https://blog.adacore.com/how-to-prevent-drone-crashes-using-...
- exdsq 5y agoI'd love to work on this sort of stuff. I'm really passionate about correct software. Can I ask how you got into the field?
- eggy 5y agoI am not in the field, this is my personal project with some others. I started programming in 1978, and I was building circuits back in the 80s and 90s with relays (ladder logic) and later with PLC's and small microcontrollers (The Parallax BASIC Stamp, PIC chips, then AVRs and others). I got into stage machinery, and the entertainment engineering industry, and I have experience with several show controller software packages. I was the "Show Manager" at "The House of Dancing Water" show in Macau for 6 years for the owner, not production, and was diving and servicing the hydraulics, electrical, and some of the aerial rigging on ropes. I also coded high-level HMIs and troubleshot low-level drive code that interfaces to the show control software. As you can imagine, a 40,000 lbf hydraulically-operated, underwater stage lifts (8 lifts with 8m stroke cylinders, 7m submerged, 1m dry) is very safety-critical when you have people on, below, and above them with multiple pinch points, etc. I know some industrial automation folk are using Elixir and Nerves with Web interfaces. I was used to QNX OS, which the show control software ran on top. Certified hardware and software is necessary to meet strict machinery and show control systems engineering. Raspberry Pis and Arduinos don't have that level of QA/QC yet, although, I have seen them patched on to systems, which to me is waiting for something to happen before it becomes a codified guideline. I am still playing with SPARK 2014 and I would be very interested if AdaCore and Ferrous Systems bring Rust up to the same ecosystem as Ada and SPARK have now. Confession: personal bias is that I am not a fan of the complexity of Rust, but syntax is Ok. I see you like Haskell. I always wished Haskell would get more practical support for control systems. I've looked into F* (not F#) as a possible piece of the puzzle. Right now, SPARK 2014 is pretty neat, and the ecosystem is a full package. I like Erlang, and I was pulling for LFE vs. Elixir, but it looks like Elixir has taken off. Nerves/Elixir looks very interesting for distributed edge-device computing with web interfaces.
- mothsonasloth 5y agoDoes this mean someone can program a AIM-120 AMRAAM missile in Rust instead of Ada? https://en.wikipedia.org/wiki/AIM-120_AMRAAM https://en.wikipedia.org/wiki/AIM-120_AMRAAM
- speed_spread 5y agoRewrite, Fire & Forget.
- goombacloud 5y agoI hope someone also picks up the work started in https://project-oak.github.io/rust-verification-tools/ https://project-oak.github.io/rust-verification-tools/ - the idea of having a `cargo verify` tool that supports different backends is great for bridging the academic PoCs with something that an average programmer can integrate into the dev workflow.
- xavxav 5y agoThat’s my long term plan, I’d like to build something like Frama-C (https://frama-c.com/ https://frama-c.com/) but for Rust, but verification tools are not like other development processes and it’s not easy to piece them together. I think that the first step is to develop a shared specification language for Rust, one that eventually could even become official like SPARK for Ada, then we move forward on integrating tools into a platform.
- touisteur 5y agoAre you aiming to translate to Why3 like SPARK and Frama-C?
- xavxav 5y agoI already do, my tool produces WhyML modules from Rust crates. But we can leverage Rust's ownership typing to drastically reduce proof obligations related to pointers and memory. Incidentally, I've started working on a VSCode frontend to Why3 to replace the existing GTK one (https://github.com/xldenis/whycode https://github.com/xldenis/whycode), I'm currently rewriting the PoC as an LSP extension. More broadly in the context of a Frama-Rust, much like Frama-C Why3 would be one of many possible backends. I specifically want abstract interpreters, test generation and other analyses to integrate and co-operate to solve proof obligations. Ie: abstract interpretation could infer a loop invariant which is then used by a deductive backend to prove the function contract. Or a deductive failure could produce a counterexample which is transformed into a test case automatically.
- 5y ago
- sitkack 5y agoThis is so wonderful that two companies so focused on reliability and safety are teaming up! > Ferrous Systems and AdaCore are announcing today that they’re joining forces to develop Ferrocene - a safety-qualified Rust toolchain, which is aimed at supporting the needs of various regulated markets, such as automotive, avionics, space, and railway. Hoping for a long, fruitful relationship! *edit, Yay!
- deleted 5y ago[deleted]