5 ms·

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

130 points by manaskarekar 9y ago

tmuir 9y ago
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.
- isaachier 9y ago
  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.
  - convolvatron 9y ago
    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.
  - richdougherty 9y ago
    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#Domain-specific_language_topics https://en.wikipedia.org/wiki/Domain-specific_language#Domai...
  - wyager 9y ago
    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.
- _delirium 9y ago
  "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".
  - dozzie 9y ago
    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.
    - deleted 9y ago
      [deleted]
    - pseudonom- 9y ago
      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.
  - tmuir 9y ago
    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.
- deleted 9y ago
  [deleted]
- Teeer 9y ago
  Just search for "Embedded Software Engineer"? https://www.indeed.com/jobs?q=embedded+software+engineer&l= https://www.indeed.com/jobs?q=embedded+software+engineer&l=
  - tmuir 9y ago
    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.
adamnemecek 9y ago
The syntax really leaves something to be desired.
- erric 9y ago
  It does seem quite a bit verbose for a simple print statement.
  - justinjlynn 9y ago
    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/ https://smaccmpilot.org/ -- a high-assurance, partially formally verified, autopilot system.
  - nickpsecurity 9y ago
    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.
    - AnimalMuppet 9y ago
      It really seems ironic to me for "embedded in Haskell" to lead to "verbose".
isaachier 9y ago
Sounds cool but hasn't been updated in months. Copyright still has 2017 for end date. Sort of implies project is no longer maintained.
- politelemon 9y ago
  It seems so - looking at their Github repo: https://github.com/GaloisInc/ivory/commits/master 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.
  - justinjlynn 9y ago
    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.
- shepmaster 9y ago
  > 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).
- ams6110 9y ago
  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/ https://galois.com/about/
nine_k 9y ago
In short: a DSL implemented in Haskell, allows to describe code with mutable state and various static guarantees around it.
cabalamat 9y ago
Their Hello World example has a lot of boilerplate.
gmueckl 9y ago
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.
- dennisdamenace 9y ago
  https://ivorylang.org/tower-overview.html 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.
  - gmueckl 9y ago
    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.
- kd0amg 9y ago
  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.
steveklabnik 9y ago
Embedded.com ran a story about Ivory and Rust recently: https://www.embedded.com/electronics-blogs/say-what-/4460422/Achieving-memory-safety-without-compromise https://www.embedded.com/electronics-blogs/say-what-/4460422...
Glawen 9y ago
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.
- AlotOfReading 9y ago
  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.
  - Glawen 9y ago
    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.
nickpsecurity 9y ago
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 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. :)

130 points by manaskarekar 9y ago

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.

isaachier 9y ago
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.
- convolvatron 9y ago
  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.
- richdougherty 9y ago
  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#Domain-specific_language_topics https://en.wikipedia.org/wiki/Domain-specific_language#Domai...
- wyager 9y ago
  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.
_delirium 9y ago
"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".
- dozzie 9y ago
  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.
  - deleted 9y ago
    [deleted]
  - pseudonom- 9y ago
    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.
- tmuir 9y ago
  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.
deleted 9y ago
[deleted]
Teeer 9y ago
Just search for "Embedded Software Engineer"? https://www.indeed.com/jobs?q=embedded+software+engineer&l= https://www.indeed.com/jobs?q=embedded+software+engineer&l=
- tmuir 9y ago
  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.

adamnemecek 9y ago

The syntax really leaves something to be desired.

erric 9y ago
It does seem quite a bit verbose for a simple print statement.
- justinjlynn 9y ago
  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/ https://smaccmpilot.org/ -- a high-assurance, partially formally verified, autopilot system.
- nickpsecurity 9y ago
  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.
  - AnimalMuppet 9y ago
    It really seems ironic to me for "embedded in Haskell" to lead to "verbose".

isaachier 9y ago

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

politelemon 9y ago
It seems so - looking at their Github repo: https://github.com/GaloisInc/ivory/commits/master 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.
- justinjlynn 9y ago
  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.
shepmaster 9y ago
> 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).
ams6110 9y ago
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/ https://galois.com/about/

nine_k 9y ago

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

cabalamat 9y ago

Their Hello World example has a lot of boilerplate.

gmueckl 9y ago

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.

dennisdamenace 9y ago
https://ivorylang.org/tower-overview.html 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.
- gmueckl 9y ago
  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.
kd0amg 9y ago
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.

steveklabnik 9y ago

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

Glawen 9y ago

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.

AlotOfReading 9y ago
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.
- Glawen 9y ago
  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.

nickpsecurity 9y ago

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