1. 15

An examination of the problems and (possible) solutions to high assurance software in embedded contexts.

  1.  

  2. 8

    Main site:

    http://ivorylang.org/

    Their Github which has tons of stuff with plenty you might find submission worthy:

    https://github.com/galoisinc

    Digging back through their blog leads to many insightful posts:

    https://galois.com/blog/

    1. 2

      Great link! Suggest security and compilers tag instead of programming. :)

      1. 2

        I disagree on compilers tag. That would make people think it’s about compiler design or techniques. There’s only a few slides about that just as a highly-abstract summary. This presentation is intended for all embedded or C programmers that might be willing to learn Haskell and Ivory to improve quality & security. It’s user-centric. So, I’d go with programming, security, and/or a QA-type tag if one existed.

        That I realized tags are for filtering as much as discovery here started to change how I do tagging. I want the right ones in to filter unwanted posts for other users' enjoyment. Yet, I’m also trying to avoid users missing good stuff by assessing their real intentions vs what’s in a submission. Perfect example here where compiler tag would be misleading for embedded developer interested in safer C but no how to do a parser. I leave tags off in such situations these days to increase serendipitous discovery.

        1. 1

          Counter-argument: the compilers tag is the closest thing we have to a PLT tag, which would’ve fit this right on the nose I believe.

          1. 1

            It just describes how to use it plus some specifics of how it works. Rust and C articles with detail do that in many cases. Compiler tag them too?

      2. 1

        Interesting stuff, but I’m interested in seeing it compared to Ada, and why (or if) they think it will see more use than Ada has

        Ada’s been around since 1983 (updated in 95, 2005, and 2013), aimed squarely at developing high assurance software in embedded systems, with lots of real world systems implemented in it.

        1. 3

          It’s more aimed at developers in safety-critical that want to distribute or work on C apps. They embed DSL’s into Haskell for its benefits. Then they extract to safe C that can be checked by existing developers and people. Basically none of these people are using or will use Ada. They know it exists given industry. Chose against it.