AdaCore and Ferrous Systems Joining Forces to Support Rust | Better HN

AdaCore and Ferrous Systems Joining Forces to Support Rust | Better HN

100 comments

xavxav4y ago

This 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) 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.

bovermyer4y ago

Verifying software used to control rocket fueling systems sounds like a good idea to me.

xavxav4y ago

That kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.

steveklabnik4y ago

> I'm curious what kinds of software they want to (eventually) verify,

https://www.reddit.com/r/rust/comments/sijixb/adacore_and_fe...

xavxav4y ago

Yea, I think that they're taking the correct approach. For certification reasons formal verification is not necessary or even really desirable, but a core hypothesis in my thesis is that we can lower the exponential factor of formal methods for Rust compared to C. The type system of Rust really helps simplify the work and I hope that Rust can be one the the languages that finally takes FV/FM 'mainstream' (it'll never be an average tool but less niche/expert).

To that end I'm always on the lookout for moderate length program components (100-1kloc) with clear safety properties that need to be verified. The standard fare is datastructures, but I'd love to see if we can expand the applications.

the__alchemist4y ago

Ferrous's embedded Rust tooling is outstanding. Ie its [Knurling 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.

Interesting, I haven't seen much chatter about their set of tooling, everything I came across about embedded programming with Rust has been about things under the rust-embedded umbrella. Do you know anything about their BLE and BLE HID support? Last time I checked rust-embedded, both were rather rudimentary.

ArgorakOP4y ago

There's rubble.

https://github.com/jonas-schievink/rubble

We've been approached by multiple parties to finish it and we are up to it, but the final effort, particularly certification is currently prohibitive. Serious inquiries taken, though - we're also happy to play "consortium" in that this does not have to be financed by any single party.

grawp4y ago

https://github.com/jonas-schievink/rubble

Their whole training is situated around BLE! https://embedded-trainings.ferrous-systems.com/beginner-work...

Edit: wrong link

ArgorakOP4y ago

Thanks for taking a moment to give that feedback!

foota4y ago

Looks like someone took inspiration from create-react-app, cool to see that kind of tooling!

I think create-react-app took inspiration from somewhere else. Plenty of skeleton project generator prior art in Rudy on Rails, Django, Turbogears, cookiecutter etc etc etc.

listic4y ago

I wish HN supported markdown, at least the links.

Grimburger4y ago

[Check this cool similar new app out HN](http:/not.suspicious.com/nor/has/tracking)

I don't, Markdown is good enough even as plain text to me

ajxs4y ago

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

ArgorakOP4y ago

I 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-joi...

zppln4y ago

I'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.

Is there going to be an announcement on the current status of Ferrocene soon? It's been almost a year since the last blog post.

In the meeting with the lang team last February, I think the consensus was that the next step would be to create a proposed charter for a project group. Did that happen?

pjmlp4y ago

The folks from Ada Core have also been playing with affine types for Ada/Spark and the ParaSail author has joined them for a couple of years now.

So it is really cool to see them working even closer with the Rust community.

touisteur4y ago

They also have a deep experience in certification and high assurance norms, which makes them an interesting partner whenever you're entering a regulated market. Not something I make use of, but I see a lot of papers/books coming from there and had deep very interesting discussions about the whole software and system safety engineering process and trust-building.

hyperman14y ago

I think the visual style of the language rubs off. There is for example

C-like: Curly brackets, small keyword count, etc ... This is a language for people who want to write fast code that gets things done, not a gram of weight too much. Hacker spirit.

Python-like: Indentation. A bit more keywords. This is a language that wants to be clear, beautiful, abstract, communicating to other readers. Academic spirit.

Cobol-like: A huge wall of text. Lots of Divisions and Organization. Bureaucratic, smells of meetings, punch cards and months of delay. Enterprise spirit.

Ada, unfortunately, looks cobol-like, so someone who knows nothing automatically assumes a ton of bureaucracy. Run away if you want work done.

Note this is purely cosmetic and has nothing to do with actual language quality.

onox4y ago

Sorry, but I disagree. Maybe in the 80s when developers were all yelling while coding :p Does this look like cobol to you?

   type GUID_String is new String (1 .. 32)
     with Dynamic_Predicate => (for all C of GUID_String => C in '0' .. '9' | 'a' .. 'f');

The only thing Ada has in common with cobol is that you can define decimal fixed point types (you specify the number of digits and a delta, which must be a power of 10) [1]

I usually use ordinary fixed point types:

   type Axis_Position is delta 2.0 ** (-15) range -1.0 .. 1.0 - 2.0 ** (-15)
     with Size => 16;

or (from wayland-ada [2]):

   type Fixed is delta 2.0 ** (-8) range -(2.0 ** 23) .. +(2.0 ** 23 - 1.0)
     with Small => 2.0 ** (-8),
          Size  => Integer'Size;

[1] https://en.wikibooks.org/wiki/Ada_Programming/Types/delta#Di... [2] https://github.com/onox/wayland-ada

touisteur4y ago

Strangely, Ada, while aimed for large-scale developments (hence the 'bureaucratic' feeling?) since conception, puts a heavy weight on readability and maintainability. No implicit shortcut operators, words instead of symbols, specific block markers (for loops, ifs, lexical block, embedded functions, ...) and explicit generic instantiation. Can be a pain to write, but it's really easier for me (whose days consist mostly of Ada, java, python, C++, C - don't ask - coding and reading) to read.

Jtsummers4y ago

> Ada, unfortunately, looks cobol-like, so someone who knows nothing automatically assumes a ton of bureaucracy. Run away if you want work done.

Ada looks nothing like COBOL., except perhaps in the most superficial sense (a bit keyword heavy compared to most other languages). The syntactic structure is really not far from what people are familiar with, in sharp contrast to COBOL. Rosettacode is a good site if you want to find some interesting (small) comparisons between languages. This is from the GCD page:

The COBOL version:

  IDENTIFICATION DIVISION.
  PROGRAM-ID. GCD.
 
  DATA DIVISION.
  WORKING-STORAGE SECTION.
  01 A        PIC 9(10)   VALUE ZEROES.
  01 B        PIC 9(10)   VALUE ZEROES.
  01 TEMP     PIC 9(10)   VALUE ZEROES.
 
  PROCEDURE DIVISION.
  Begin.
      DISPLAY "Enter first number, max 10 digits."
      ACCEPT A
      DISPLAY "Enter second number, max 10 digits."
      ACCEPT B
      IF A < B
        MOVE B TO TEMP
        MOVE A TO B
        MOVE TEMP TO B
      END-IF
 
      PERFORM UNTIL B = 0
        MOVE A TO TEMP
        MOVE B TO A
        DIVIDE TEMP BY B GIVING TEMP REMAINDER B
      END-PERFORM
      DISPLAY "The gcd is " A
      STOP RUN.

The Ada version:

   function Gcd (A, B : Integer) return Integer is
      M : Integer := A;
      N : Integer := B;
      T : Integer;
   begin
      while N /= 0 loop
         T := M;
         M := N;
         N := T mod N;
      end loop;
      return M;
   end Gcd;

The C version on that page demonstrates what I'd consider a bad practice, but I'll show it and how a clearer version might be written:

  static int gcd(int a, int b)
  {
    while (b != 0) b = a % (a = b); // not clear at all, good way to avoid a temporary variable
    return a;
  }
  static int gcd(int a, int b)
    int t;
    while (b != 0) {
      t = b;
      b = a % b;
      a = b;
    }
    return a;
  }

Compared to Ada, that second C one is 3 lines shorter, which corresponds to the lack of `begin` and reusing the parameter variables rather than defining two new local variables for the loop. Ada doesn't permit you to assign to "in" parameters, which is the default.

http://rosettacode.org/wiki/Greatest_common_divisor

ajdude4y ago

It's kind of the opposite for me. It takes much less time to understand what Ada-written code is doing compared to any of the C-type languages, or even Rust. It is very plainly written. Verbose, yes, but much more plainly written.

Just take a look at this, and tell me it's not legible: https://github.com/joakim-strandberg/advent_of_code/blob/mas...

mamcx4y ago

The Pascal family could benefit by a bit more of brevity, but I trade the syntax of it to C-like langs like Rust any day. They are not that less verbose at the end: Is only in the "small" that look compact.

0xDEEPFAC4y ago

> Ada, unfortunately, looks cobol-like, so someone who knows nothing automatically assumes a ton of bureaucracy. Run away if you want work done.

The Ada++ project (a modified GNAT compiler) might interest you then.

http://www.adapplang.com/

pjmlp4y ago

This are big news, congratulations to everyone making this happen!

Looking forward to what it might bring into safer computing world.

nix234y ago

I have no connections to AdaCore, but the products are absolutely great (especially GNAT community edition).

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

ArgorakOP4y ago

I can share from Ferrous side that the partnership started "clicking" when we found our common interest in product quality and user service.

Vayl4y ago

As a newbie dev I find the work you do quite inspiring, super cool to see you here ! (Just followed you on Twitter coincidentally)

goombacloud4y ago

I hope someone also picks up the work started in 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.

xavxav4y ago

That’s my long term plan, I’d like to build something like Frama-C (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.

touisteur4y ago

Are you aiming to translate to Why3 like SPARK and Frama-C?

mothsonasloth4y ago

Does this mean someone can program a AIM-120 AMRAAM missile in Rust instead of Ada?

https://en.wikipedia.org/wiki/AIM-120_AMRAAM

speed_spread4y ago

Rewrite, Fire & Forget.

brabel4y ago

Can we get a Rust version of Spark now? I think that would be really cool!

eggy4y ago

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

exdsq4y ago

I'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?

pabs34y ago

Is Ferrocene going to be open source?

steveklabnik4y ago

I don't know if the plans have changed, but originally: 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/hv9cpn...

eggy4y ago

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

This 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!

guerby4y ago

Soon a "pragma Import (Rust, MyFunction);" ? :)

ArgorakOP4y ago

Let'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.

j / k navigate · click thread line to collapse