AdaCore and Ferrous Systems Joining Forces to Support Rust | Hacker News Reader

AdaCore and Ferrous Systems Joining Forces to Support Rust

blog.adacore.com

357 pointsArgorak100 comments

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.

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

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

what are those tools written in?

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

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

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

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

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.

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.

I wish HN supported markdown, at least the links.

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

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

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

That doesn't work on touchscreens.

Edit: Commenters say long-pressing reveals a URL without opening it in mobile browsers, which is nice to know. I only have experience with using regular desktop FF on my (Linux) phone, which doesn't support such a thing AFAICT.

no, but at least here on Fx mobile, i can long-tap and see where it's going.

Worked fine on mine (chrome on Android): touch and hold and wait for pop up. If the link in the upper right is cut short with an ellipsis, touching the link will expand it, just like ellipsis shortened alt texts.

Depends on the device and software. At least on my phone's Firefox browser a long-press of a link will bring up a menu that includes the URL (though it can run into space constraints for long URLs).

On iOS, that loads the page in a pop-over window.

How about altering how the Markdown would be rendered?

E.g., the previously mentioned input:

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

Could be rendered as:

  <a class="link-display" href="http:/not.suspicious.com/nor/has/tracking">Check this cool similar new app out HN</a>
  <span class="link-content">[not.suspicious.com]</span>
  
  .link-display {
    /* Whatever styling you want for the link itself. */
    font-weight: bold;
  }
  
  .link-content {
    /* A more in-your-face helper that shows at least the domain. */
    font-style: italic;
    opacity: 0.5;
  }

Example: https://jsfiddle.net/upb7o0zm/

I'm not sure if the markdown spec mandate what the output should be, but I indeed love you idea!

Copy-paste-friendly version:

    <a class="link-display" data-host="not.suspicious.com" href="http://not.suspicious.com/nor/has/tracking">Check this cool similar new app out HN</a>

    .link-display:after {
        content: " [" attr(data-host) "]";
    }

Between homoglyphs and HN eliding long links, you can do the same without markdown.

Thanks for taking a moment to give that feedback!

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.

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.

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

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

Edit: wrong link

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.

I'm just a hobbyist, so certification is less important for me as long as it works for what I need. BLE 5 would be nice but more important to me is an HID service that's fairly complete, but that doesn't even seem to be on the roadmap. It's going to be quite a pain if I had to implement this myself.

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.

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

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.

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

Interesting, thanks. The reason I ask is that in my experience you don't malloc mid-flight so to speak (for WCET/WCRU reasons, among others), so Rust's guarantees there are largely irrelevant. It's a pretty opaque area of the software industry though, so others may have come to other conclusions.

I'm not working in safety critical systems, but our embedded OS doesn't do any dynamic memory allocation at all, and Rust still helps quite a bit even without that.

https://cliffle.com/blog/on-hubris-and-humility/

DO-178C has writing and requirements around dynamic memory management. (DO-332 / ED-217, OO.D.1.6)

Rust also can also model other things through ownership, like passing a device handle safely between components, to avoid concurrent use.

Thanks, I wasn't aware of DO-332 actually. I'll have to see if it's available through work. It's always interesting to think about how things can be done differently and where the tradeoffs would be. :)

Feel free to reach out, it's a topic of interest to us. A good place to discuss is for example the AeroRust Discord or just send me an email. https://github.com/AeroRust/Welcome

Rust has the same advantages in malloc-free environments as well. Dangling pointers can still be a thing in non-malloc code.

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

This may interest you: "In this document, we show how SPARK can be used to achieve high code quality with guarantees that go beyond what would be feasible with MISRA C."

https://www.adacore.com/uploads/books/pdf/SPARK-Ada-for-MISR...

Compared to most other languages that focus on correctness, Rust performs better. If you don't need performance, probably one of the other alternatives is better. However Rust may be unique in preventing data races at compile time, which could be a huge boon in some applications.

I suppose languages like Haskell maybe accomplish that as well, since you never mutate state at all?

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?

First question: yes. It was hard to talk about the current state of Ferrocene with all the things ongoing last year. Now that I have more bandwidth and we found a development beat, you can also expect more regular updates.

Second question: that was the discussion about higher assurances in the compiler in general. The group did not form, but that's on the project side, where I'm not part of anymore. We're very ready to participate there though.

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.

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.

Fully agree. I also occasionally read stuff on high integrity computing, very interesting material that the industry at large still is far behind of what could be in practice.

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.

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.

A lot of this has been much-improved with Ada 2022 and recent changes. Notably, lambdas, pattern matching, less-verbose operators, etc.

https://blog.adacore.com/going-beyond-ada-2022

You say 'improved' but I feel it doesn't always go the 'more readable' way. I'm very much not a fan of the 'dot notation' and still like to use named parameters, and force explicit types instead of the creeping auto trend. I read much more code than I write and I'm feeling... not heard on the recent changes to ease code writing. At least I can write libadalang scripts (or langserv one day 'to right-click add back what I need in for-of loops, or dot-notation.

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

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

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.

Maybe a bit like this? https://github.com/Lucretia/orenda/blob/master/samples/modul...

Yeah, not bad.

Another one, because look like you are looking for inspiration:

https://www.elementscompiler.com/elements/oxygene/language.a...

Yeah, I remember seeing that years ago, shame it's not open and only win/mac.

> 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/

Have you had a release since last April 1st? Or fixed the ugly case statement?

  case Variable: -- <====
    when 0      => Put_Line ("Zero");
    when 1 .. 9 => Put_Line ("Positive Digit");
    when 10 | 12 | 14 | 16 | 18 =>
      Put_Line ("Even Number between 10 and 18");
    when others => Put_Line ("Something else");
  } -- <====

Matching : with } does not make for clearer code.

What other suggestions do you have besides changes to the case statements?

Ada++ makes two changes to the Ada language. First, it changes some keywords into new keywords or symbols, but in a gross way (the case example, is becomes : as a blanket rule, even when it leads to : being paired with }). This could be done by a (tedious) awk program or sed script. The second change it makes is that use will also with a package, that's a nice ergonomic feature. But it's the only thing of modest complexity that it does to change the language. There are no other enhancements to the language that it introduces that make it a compelling thing or an obvious non-joke (it's release date for 0.2.0 was 1 April 2021).

The actual Ada developers are focused on actual language enhancements with the Ada 2022 standard and increasing the scope of properties that SPARK (a proper subset of Ada now) can prove about a program. Including approaching some of the properties that people find desirable with Rust's borrow checker and lifetime analysis. Ada++ should be doing things like that, meaningfully improving the language and not just being a glorified awk program that doesn't change or add any real syntactic or semantic properties of the language. Also, the author should stop doing releases on April Fool's Day if they really want to be taken seriously.

It is an April Fools Day joke. They forked GCC and made one commit on April Fools Day 2021, and haven't touched it sense.

Compare:

Ada++ -- https://github.com/AdaPlusPlus/gcc/commits/master

GCC 10 (history from April 2021) -- https://github.com/gcc-mirror/gcc/commits/releases/gcc-10?af...

While I agree, the person I initially responded to has, in the past, asserted that they made it and that it is not a joke. They've remained committed to it for a couple years now and have, at times, misled or attempted to mislead people into thinking it was a serious effort. So when I catch them trying to do it again, I call them out.

https://news.ycombinator.com/item?id=29081047

It seems that they are either ludicrously committed to the joke, or have convinced themselves that it's a serious effort despite all evidence to the contrary.

The joke was on AdaCore's website.

? When was Ada++ ever on AdaCore's site?

I didn't say it was.

https://blog.adacore.com/a-modern-syntax-for-ada

Well, I think my confusion was reasonable since the previous comments were all about Ada++ (the joke that 0xDEEPFAC has decided is serious).

> 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

This is one of those post where I'm happy to see so much people disagreeing, except I'm not sure we're disagreeing. Your key sentence is: ... except in the most superficial sense... That is exactly the barrier Ada needs to overcome. If people take the time to really look at Ada,they'd see its actually quite reasonable.

But if someone asks what language to learn, they start with shortening the almost infinite list of languages to something worth looking at. This filtering process happens in the crudest possible way, based more on feelings and hearsay than on verified facts: How big is the ecosystem, how will other people look at my code, ... This proces delivers, say, about 10 to 20 languages worth actually spending time looking at them. That's the hurdle Ada has to jump. This is a marketing problem.

If you look at rust, the work done by Mozilla and people like e.g. Steve Klabnik to put the language on the map is enourmously valuable. With code examples, blog post, fixing real world pain points, answering questions, .... It took years but they did it. If Ada had a group of people and a bigname organization, all doing this work, it would be a completely different story.

Agreed, but the problem you're describing has nothing to do with looking like COBOL. If we're talking superficial syntax, my first thought was that it looks like Ruby but with C++-style interface/implementation separation. The syntax is odd, but not at all unpleasant.

For me, my hurdles were:

* First, I thought that Ada was exclusively a proprietary language.

* Then, I got confused about whether I can use GNAT Community and not publish it under the GPL (https://www.adacore.com/get-started says I must).

* Finally I found FSF GNAT (http://www.getadanow.com/), so it turns out there is a standard-licensed language I can use.

At this point I'm finally ready to actually try Ada, and just haven't started a project that seemed like a good fit. But the bulk of my barrier to entry was licensing questions, not syntax.

See https://pyjarrett.github.io/programming-with-ada/clearing-th...

Yep! This is the tutorial that finally cleared everything up for me. I'd previously found AdaCore.com, which was where I learned about the Community edition but not the FSF GNAT.

You can use any version of gnat to build this - https://github.com/Lucretia/sdlada

I'm disagreeing with the assertion that Ada looks like COBOL. You may or may not agree with that statement, but you made it.

> This filtering process happens in the crudest possible way, based more on feelings and hearsay than on verified facts

And that's why people should stop making statements like:

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

Without much stronger caveats to clarify that it is not a correct impression. Without a strong statement clarifying that it's only an impression (based on the most superficial of analyses) and not the reality, people will read comments like yours (and others in threads like this one) and never go any further to realize that they're false, and end up repeating them.

In an Ada thread just a few weeks back someone wrote COBOL-ish code claiming it was Ada code. It was a math-y example like the GCD code above, and clearly wouldn't work if you had even a passing familiarity with Ada. But it was written in such strong terms that it gave the impression the author was competent when they were really ignorant.

> If you look at rust, the work done by Mozilla and people like e.g. Steve Klabnik to put the language on the map is enourmously valuable. With code examples, blog post, fixing real world pain points, answering questions, .... It took years but they did it. If Ada had a group of people and a bigname organization, all doing this work, it would be a completely different story.

AdaCore has actually done a lot of the same.

http://learn.adacore.com - really good learning resources, freely available

https://blog.adacore.com - active blog describing various Ada-based projects as well as developments in SPARK and Ada.

And as an answer to things like Cargo there's now Alire:

https://alire.ada.dev

Both comp.lang.ada and r/ada are pretty active.

> That is exactly the barrier Ada needs to overcome

No, this is the barrier people need to overcome. Readable is good.

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

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

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

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

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

Thanks :).

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

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.

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.

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

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

That looks amazing. You should shoot an email to Yannick Moy! He had lots of insights and ideas on how to help automatically generate or infer (reliably) loop variants/invariants (they use loop unrolling for example: https://blog.adacore.com/proving-loops-without-loop-invarian...) .

I know AdaCore uses CodePeer (abstract interpretation and iirc 'interval propagation') to help SPARK avoid or simplify some VCs and it helps in a lot of cases.

There's also some possibilities with symbolic execution, maybe on the counter-examples generation side.

I think you're treading a very interesting path!

I've talked to Yannick quite a lot in the past as my lab develops Why3 and SPARK uses my translation for their new support for pointers (access types).

Additionally, my advisor collaborates with them on counterexample generation, especially with managing to get readable counterexamples out from the SMT. We've toyed a little with invariant generation but its very tricky to get something actually usable. Additionally, I have the personal (soft) requirement that the generated invariant should be injected into the source code and not purely internal / hidden.

I confirm that we're following closely what Xavier is doing for Rust, and even copied his work on "prophecy variables" to take the effects of borrowing into account in loop invariants in SPARK!

Your plans for having Rust analyzers collaborate look very cool! Like you said, the first challenge is to agree on a base specification language. I hope this gets discussed at the next Rust Verification Workshop.

Hi Yannick. Good to see so much collaboration in the FM world.

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

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

Rewrite, Fire & Forget.

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

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

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?

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

Is Ferrocene going to be open source?

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.

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

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!

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

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.

Reply on news.ycombinator.com