1. 4
  1.  

  2. 2

    Oh, I’m one of the editors of this! Happy to answer questions.

    1. 1

      Section 3.5.1 “What would you like to see in the abstract machines of new languages to facilitate interoperability?” mentions the JVM, CLR, and WASM intermediate representations - but these are viewed as providing insufficient guarantees. Did anyone at your symposium have experience with IELE?

      1. 1

        It wasn’t discussed. I have a tiny bit of experience with the previous Etherium VM, which was very slow (which was fine, because it wasn’t intended as a general-purpose compute substrate). From a 2-minute skim, it looks pretty interesting:

        • Basic-block-based control flow (arbitrary graph within a function) is much easier to generate than Wasm.
        • Memory looks like it’s easy to have a lot of distinct objects.

        The second one means that it ends up looking like a segmented architecture, so it would be a better compilation target for PL/M than C, so I’m not sure how easy it would be to lower arbitrary code into the VM (I guess that’s a non-goal if it’s intended for smart contracts?).

        1. 1

          I have a tiny bit of experience with the previous Etherium VM, which was very slow

          IELE was developed in response to the Ethereum foundation asking Grigore Rosu what he thought of replacing the EVM with WASM. It’s based on LLVM’s architecture (both projects come from the University of Illinois) and their verified implementation is apparently competitive with an unverified implementation (my memory is hazy, at least within an order-of-magnitude and probably better by now).

          I’m not sure how easy it would be to lower arbitrary code into the VM

          I’m not a real CS major (so I wouldn’t be able to investigate directly) but I get the sense that its suitability as a compilation target is dictated by their sources of funding, which is dominated by cryptocurrencies ATM. They previously formalized a handful of languages in their K framework (Java, C, JavaScript, LLVM, etc) so they have plenty of experience with polyglot language development.

          You should invite them to the next conference. They are very bullish on small-step semantics for mainstream adoption of verification and for an IR like IELE as the best place to do that.

          1. 1

            Thanks for the pointer, it looks very interesting. I don’t know if there will be another Secure Compilation Dagstuhl, it depends on the feedback. I probably won’t be an organiser next time if there is (though I hope to attend).