1. 12

  2. 3

    Nice find! I wish I knew of more projects using Standard ML. https://en.wikipedia.org/wiki/Standard_ML#Major_projects_using_SML doesn’t have much to say.

    1. 3

      One advantage in high-security is different projects have developed many pieces of an overall vision of SML that would make it a fierce contender for non-high-performance apps at EAL5 equivalent. There’s its base properties of safety, a concurrent version, a version for information flow (esp covert channels), maybe contracts in one, a QuickCheck port, embeddings in LISP’s for RAD style, an optimizing compiler for untrusted code, a verifying compiler for trusted code, integration with provers, and some neat stuff I cant recall but know I read. Blurry.

      These pieces could be combined into something that had the advantages of each plus knobs to turn things on or off depending on users’ needs. I’ve always said SML or Ocaml with a Ocaml-SML translater woukd be a great standard for tool development in any project supporting efforts where we prefer every component to be trustworthy. The empirical evidence leans if favor of this with all the compilers and other analysis/transform tooling written fairly-reliably in ML’s. Highest examples outside extracted code like CompCert would be things like Esterel’s code generator they said Ocaml aided a lot on source-to-object verification plus general correctness.

      1. 2

        There’s the Standard ML github org, though many of those projects seem stale. Check the project page, too, for more links (also sometimes stale). On the one hand, some of those links are stale because SML is long stable and the software is functional and complete. On the other hand, some of those links are stale because SML is stale and the community is small and transient (lots of folks use SML during college and then drop off after those few years).

      2. 3

        I love the idea of languages with good multi-stage compilation stories.

        For example, being able to say “compile up everything, let me check my model definitions, then do some more code generation based off of new known facts” is powerful. It makes a lot more static analysis possible.

        A bit unfortunate that a lot of lisps have this but don’t have the nicest static analysis tools to go with them