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.

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

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

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

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.

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

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.

  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");
  } -- <====

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