[HN Gopher] AdaCore and Ferrous Systems Joining Forces to Suppor...
___________________________________________________________________
AdaCore and Ferrous Systems Joining Forces to Support Rust
Author : Argorak
Score : 347 points
Date : 2022-02-02 07:36 UTC (15 hours ago)
(HTM) web link (blog.adacore.com)
(TXT) w3m dump (blog.adacore.com)
| goombacloud wrote:
| 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.
| xavxav wrote:
| 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.
| touisteur wrote:
| Are you aiming to translate to Why3 like SPARK and Frama-C?
| xavxav wrote:
| 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.
| touisteur wrote:
| 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!
| xavxav wrote:
| 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.
| yannickmoy wrote:
| 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.
| touisteur wrote:
| Hi Yannick. Good to see so much collaboration in the FM
| world.
| sitkack wrote:
| 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!
| xavxav wrote:
| 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.
| steveklabnik wrote:
| > I'm curious what kinds of software they want to (eventually)
| verify,
|
| https://www.reddit.com/r/rust/comments/sijixb/adacore_and_fe...
| xavxav wrote:
| 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.
| bovermyer wrote:
| Verifying software used to control rocket fueling systems
| sounds like a good idea to me.
| xavxav wrote:
| That kind of software is not usually written in Rust (or
| Ada), but using Simulink / SCADE or other model-based and
| synchronous tools, afaik.
| gameswithgo wrote:
| what are those tools written in?
| fgh wrote:
| 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).
| bluGill wrote:
| 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.
| pabs3 wrote:
| Is Ferrocene going to be open source?
| steveklabnik wrote:
| 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...
| eggy wrote:
| 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.
| nix23 wrote:
| I have no connections to AdaCore, but the products are absolutely
| great (especially GNAT community edition).
| touisteur wrote:
| (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.
| Argorak wrote:
| I can share from Ferrous side that the partnership started
| "clicking" when we found our common interest in product quality
| and user service.
| Vayl wrote:
| As a newbie dev I find the work you do quite inspiring, super
| cool to see you here ! (Just followed you on Twitter
| coincidentally)
| Argorak wrote:
| Thanks :).
| pjmlp wrote:
| This are big news, congratulations to everyone making this
| happen!
|
| Looking forward to what it might bring into safer computing
| world.
| brabel wrote:
| Can we get a Rust version of Spark now? I think that would be
| really cool!
| eggy wrote:
| 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-...
| exdsq wrote:
| 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?
| [deleted]
| ajxs wrote:
| 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.
| hyperman1 wrote:
| 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.
| mamcx wrote:
| 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.
| Lucretia9 wrote:
| Maybe a bit like this? https://github.com/Lucretia/orenda/b
| lob/master/samples/modul...
| Jtsummers wrote:
| > 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
| hyperman1 wrote:
| 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.
| Jtsummers wrote:
| 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.
| Lucretia9 wrote:
| > That is exactly the barrier Ada needs to overcome
|
| No, this is the barrier _people_ need to overcome.
| Readable is good.
| lolinder wrote:
| 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.
| Lucretia9 wrote:
| You can use any version of gnat to build this -
| https://github.com/Lucretia/sdlada
| pyjarrett wrote:
| See https://pyjarrett.github.io/programming-with-
| ada/clearing-th...
| lolinder wrote:
| 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.
| onox wrote:
| 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
| ajdude wrote:
| 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...
| touisteur wrote:
| 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.
| gavinray wrote:
| 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
| touisteur wrote:
| 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.
| 0xDEEPFAC wrote:
| > 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/
| Jtsummers wrote:
| 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.
| exitcode0 wrote:
| What other suggestions do you have besides changes to the
| case statements?
| Jtsummers wrote:
| 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.
| lolinder wrote:
| 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...
| Jtsummers wrote:
| 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.
| Lucretia9 wrote:
| The joke was on AdaCore's website.
| Jtsummers wrote:
| ? When was Ada++ ever on AdaCore's site?
| Lucretia9 wrote:
| I didn't say it was.
|
| https://blog.adacore.com/a-modern-syntax-for-ada
| Jtsummers wrote:
| Well, I think my confusion was reasonable since the
| previous comments were all about Ada++ (the joke that
| 0xDEEPFAC has decided is serious).
| pjmlp wrote:
| 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.
| touisteur wrote:
| 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.
| pjmlp wrote:
| 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.
| Argorak wrote:
| 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...
| zppln wrote:
| 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.
| Argorak wrote:
| 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).
| zppln wrote:
| 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.
| Argorak wrote:
| 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.
| zppln wrote:
| 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. :)
| mlindner wrote:
| Rust has the same advantages in malloc-free environments
| as well. Dangling pointers can still be a thing in non-
| malloc code.
| steveklabnik wrote:
| 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/
| gmfawcett wrote:
| > 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...
| gameswithgo wrote:
| 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?
| mjw1007 wrote:
| 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?
| Argorak wrote:
| 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.
| [deleted]
| mothsonasloth wrote:
| 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_spread wrote:
| Rewrite, Fire & Forget.
| [deleted]
| the__alchemist wrote:
| 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.
| listic wrote:
| I wish HN supported markdown, at least the links.
| izietto wrote:
| I don't, Markdown is good enough even as plain text to me
| Grimburger wrote:
| [Check this cool similar new app out
| HN](http:/not.suspicious.com/nor/has/tracking)
| masklinn wrote:
| Between homoglyphs and HN eliding long links, you can do
| the same without markdown.
| littlestymaar wrote:
| 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).
| KronisLV wrote:
| 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/
| littlestymaar wrote:
| I'm not sure if the markdown spec mandate what the output
| should be, but I indeed love you idea!
| Arnavion wrote:
| 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)
| "]"; }
| Arnavion wrote:
| 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.
| Tistron wrote:
| no, but at least here on Fx mobile, i can long-tap and
| see where it's going.
| froh wrote:
| 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.
| KwanEsq wrote:
| 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).
| smarx007 wrote:
| On iOS, that loads the page in a pop-over window.
| [deleted]
| Argorak wrote:
| Thanks for taking a moment to give that feedback!
| foota wrote:
| Looks like someone took inspiration from create-react-app, cool
| to see that kind of tooling!
| wyuenho wrote:
| 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.
| wyuenho wrote:
| 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.
| grawp wrote:
| https://github.com/jonas-schievink/rubble
|
| Their whole training is situated around BLE!
| https://embedded-trainings.ferrous-systems.com/beginner-
| work...
|
| Edit: wrong link
| Argorak wrote:
| 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.
| wyuenho wrote:
| 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.
| guerby wrote:
| Soon a "pragma Import (Rust, MyFunction);" ? :)
| Argorak wrote:
| 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.
___________________________________________________________________
(page generated 2022-02-02 23:02 UTC)