Ivory: an embedded domain-specific language for safer systems programming | Hacker News Reader

Ivory: an embedded domain-specific language for safer systems programming

ivorylang.org

130 pointsmanaskarekar32 comments

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.

The landing page is a bit disappointing in that regard. I'd rather see example programs for listening on a socket or setting up a piped parent/child pair than computing Fibonacci numbers. I guess the fib_loop example at least demonstrates that mutable state is readily accessible (not what you'd necessarily expect in a Haskell eDSL), but I think for a domain-specific language it would be better salesmanship to demonstrate a domain-related task.

https://ivorylang.org/tower-overview.html

> The Tower Language is an eDSL for composing Ivory programs into real-time systems. Tower programs specify communication channels, tasks, and signal handlers, and generate Ivory code which implements scheduling and communication for real-time operating systems.

Interesting! This seems to be in very early development. I do not fully understamd the simple example, but somehow the basic idea and delarative nature feels promising to me. I do not have a good enough understanding of this. I fear that a single central declaration of all the tasks and communication channels might get unwieldy for a system with realistic complexity.

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.

It's probably because memory issues are simultaneously one of the simplest, most easily-defined issues to solve and also potentially quite severe.

The more important issues we face are also significantly more difficult to solve with a simple tool, so there's correspondingly fewer solutions to even look at and they're often more disruptive to test than a new language.

Indeed.

Anyway i would love to have an open source Simulink-like IDE which generates C code. There is currently not much choices in model based tool, and none are open source.

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

> Copyright still has 2017 for end date.

I don't know about this project, but unmaintained copyright years has been the case in almost every project that I've taken the time to look at (and that has them). Unless a project has an active legal team, I wouldn't use such dates to mean anything (for better or worse).

It seems so - looking at their Github repo: https://github.com/GaloisInc/ivory/commits/master

Have a look at the pull requests and issues, I'm wondering if this may be an internal project from GaloisInc but not actively maintained externally.

Indeed. Galois have a reputation, at least in the Haskell community, for designing, building and releasing really cool stuff -- but then not maintaining it for much longer than the internal project requires. Galois is primarily a consulting firm and the amount of time they have for projects depends greatly on how useful they are to their current consulting arrangements. That said, I don't speak for them in any capacity -- these are only my personal observations.

The project is developed by Galois. From their website[1], "Galois is a privately held U.S.-owned and -operated company established in 1999 in Portland, Oregon."

So they started at probably one of the worst times to start a tech company (right at the dot-com bust) and are still around.

That says nothing about whether Ivory will get any traction, but at least there's an apparently stable company behind it.

[1] https://galois.com/about/

The syntax really leaves something to be desired.

It does seem quite a bit verbose for a simple print statement.

Ivory is not for print statements. Ivory is for designing and implementing high-reliability/safety-critical/hard-real-time firmwares. Combined with their Tower project, and other support projects, it's used to build https://smaccmpilot.org/ -- a high-assurance, partially formally verified, autopilot system.

To add to other comment, the main goals of high assurance systems are twofold:

1. Design systems that either never fail in field or fail safe. Many also want recovery mechanisms that always work.

2. Part many miss: convince other people from buyers to regulators they did No 1.

One reason both Ada and formal specifications are so verbose is that lots of detail that's implicit in lots of languages are explicit in them so they can be reviewed. People overlooking detail due to verbosity is a common problem. People in this industry are disciplined enough to look at stuff in detail, though. So, the tradeoff of languages in this field is to optimize for software being read by people who want no stone unturned.

Now, what I cant tell you is how much verbosity is due to it being embedded in Haskell or just its own design. Verbosity doesnt surprise me, though.

It really seems ironic to me for "embedded in Haskell" to lead to "verbose".

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.

Actually even the use of embedded here is somewhat ambiguous. Embedded as in devices, or embedded as in embedded within another programming language. I think it might mean the latter here.

but the text specifically says 'for interacting with hardware'. it would be instructive if there was a simple hardware interface example on the front page instead of just hello world and fib.

You are correct. The first bullet point on the page defines what embedded means for Ivory.

> Embedded: Ivory is implemented as a library of the Haskell programming language. Ivory programs are written using Haskell syntax and types.

An "embedded DSL" is written inside a host language. It is different from a DSL which is parsed from characters using an interpreter or compiler.

I agree it's a confusing term in this context. I've also used the term "hosted". Wikipedia also suggests "internal". https://en.wikipedia.org/wiki/Domain-specific_language#Domai...

It’s both. Ivory is a Haskell EDSL for programming hard real-time embedded systems. Iirc they originally created it for a DARPA aerospace software contract.

"Embedded DSL" is for better or worse a reasonably well established term for DSLs that are embedded within a host language using the language's own abstraction constructs (libraries, macros, etc.), rather than being implemented as a separate language with a parser and compiler/intepreter. I do usually use the alternative term "internal DSL" though, which I believe is also the older one. Besides avoiding the name clash with embedded programming in the low-level hardware sense, I like it better because the opposite of an internal DSL is an external DSL, not an "unembedded DSL".

Much better term is to call it what it is: a domain-specific API, instead of bending the term that was not supposed to be used like this.

An EDSL and a domain-specific API are not the same thing. For example, one typically expects the description of a program's logic and its execution to be separate in a DSL (i.e. building up expressions from the syntax made available in the EDSL and then later applying an interpreter (possibly multiple interpreters) to these expressions) while this is not generally true for domain-specific APIs.

I do in fact have a horse in this race as an Embedded developer, but I don't really ascribe worthiness of exclusive use of the term to any particular side. Theyre all just using a term that predates all of their industries, so this isn't a thing to pick or defend sides on, in my opinion. I simply lament the inability to be specific and comprehensive. It's not like "Embedded" is even a hot buzzword or has anything resembling unique brand recognition.

Just search for "Embedded Software Engineer"?

https://www.indeed.com/jobs?q=embedded+software+engineer&l=

Correct me if I am wrong, but adding terms to the query can have two distinct effects:

Either this would add jobs that hit "software" or "developer" in isolation,(see original problem) or it would filter out "Embedded programmer" or "Embedded systems engineer", if those ads didn't include all three individual terms "embedded", "software", and "developer". (Why I tolerate my current approach)

I've always assumed I was casting the optimally sized net with a single keyword, and no better alternative existed for purposes of completeness.

Reply on news.ycombinator.com