AdaCore and Ferrous Systems Joining Forces to Support Rust(blog.adacore.com) |
AdaCore and Ferrous Systems Joining Forces to Support Rust(blog.adacore.com) |
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.
https://www.reddit.com/r/rust/comments/sijixb/adacore_and_fe...
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.
These make flashing and debugging Rust embedded very easy - easier than any embedded toolchain I've seen besides Arduino.
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.
Their whole training is situated around BLE! https://embedded-trainings.ferrous-systems.com/beginner-work...
Edit: wrong link
Looking forward to what it might bring into safer computing world.
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 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.
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-...
> 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...
> 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!
I expressed some of those thoughts in the corresponding post on the Ferrous Systems blog: https://ferrous-systems.com/blog/ferrous-systems-adacore-joi...
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?
So it is really cool to see them working even closer with the Rust community.
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.
type GUID_String is new String (1 .. 32)
with Dynamic_Predicate => (for all C of GUID_String => C in '0' .. '9' | 'a' .. 'f');
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;
type Fixed is delta 2.0 ** (-8) range -(2.0 ** 23) .. +(2.0 ** 23 - 1.0)
with Small => 2.0 ** (-8),
Size => Integer'Size;
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.
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;
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;
}
Just take a look at this, and tell me it's not legible: https://github.com/joakim-strandberg/advent_of_code/blob/mas...
The Ada++ project (a modified GNAT compiler) might interest you then.
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.
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.
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.
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.
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!
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.
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");
} -- <====
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.
Another one, because look like you are looking for inspiration:
https://www.elementscompiler.com/elements/oxygene/language.a...
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).
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...
Rust also can also model other things through ownership, like passing a device handle safely between components, to avoid concurrent use.
I suppose languages like Haskell maybe accomplish that as well, since you never mutate state at all?
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.
> 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:
Both comp.lang.ada and r/ada are pretty active.
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.
No, this is the barrier people need to overcome. Readable is good.
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).
E.g., the previously mentioned input:
[Check this cool similar new app out HN](http:/not.suspicious.com/nor/has/tracking)
<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;
}
<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) "]";
}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.
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.
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...
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.