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.
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.
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.
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.
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.
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.
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).
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;
}
<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.
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).
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'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.
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).
> 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."
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.
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
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.
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.
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;
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.
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.
> 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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'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.
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!
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.
> 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.
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.
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.
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.