Galois is essentially a commercial R&D lab for businesses and governments. Although having trouble a while back, this business model plus talent at solving problems has landed them steady contracts. Even better, they open source lots of their tools they use for high-assurance software. Ivory's main use that I know of is SMACCMPilot program for high-assurance drone. They give details some of you want here:

https://smaccmpilot.org/software/properties.html

Also, check out their blog, Github, and talks for lots of interesting stuff. In case anyone wonders, I have no affiliation with them: just a high-assurance researcher that gives props to those in field doing solid work, esp if FOSS-friendly. :)

Embedded.com ran a story about Ivory and Rust recently: https://www.embedded.com/electronics-blogs/say-what-/4460422...

I have not dug into this, but I am curious: how would you write multiple interacting, concurrent, timing-sensitive tasks with this? I am thinking about things like multiple complex protocol stacks on top of different interrupt driven I/o ports (uart, I2C, SPI) in parallel with a main application that is supervised by a watchdog.

In short: a DSL implemented in Haskell, allows to describe code with mutable state and various static guarantees around it.

Their Hello World example has a lot of boilerplate.

I do not understand the focus on memory corruption, it is not the major problem in embedded development. In my experience, the vast majority of problems were due to logic failures. Sometimes there was a buffer overflow which was detected in an old function when something new was implemented somewhere else..

For me the way to go are tools like matlab simulink to better figure out a complex program, and not yet another language trying to catch memory corruption bugs.

Sounds cool but hasn't been updated in months. Copyright still has 2017 for end date. Sort of implies project is no longer maintained.

The syntax really leaves something to be desired.

Searching for embedded development jobs by the keyword "embedded" is already an exercise in manually filtering out phlebotomist jobs, teaching positions, histotechnologists, all sorts of people who think they're differentiating their offered position by saying "embedded with a team", as if thats functionally different from "working with people". Now weve added functional programmers.

Yet it remains by far the most relevant keyword in my experience. I would think "firmware" would be a better, or at least sufficient catch-all.