grosu
commented
5 years ago See https://github.com/runtimeverification/iele-semantics/blob/master/Design.md for the design rationale behind IELE and how it differs from the EVM.
Open grosu opened 5 years ago
grosu
commented
5 years ago See https://github.com/runtimeverification/iele-semantics/blob/master/Design.md for the design rationale behind IELE and how it differs from the EVM.
The VM comparison page, https://github.com/ewasm/design/blob/master/comparison.md is really important and interesting. I would recommend you guys to add a link to IELE under the LLVM section, because IELE is for LLVM what eWASM is meant to be for WASM: https://github.com/runtimeverification/iele-semantics. It can just as well be called eLLVM.
We'd be glad to take and answer any questions that you guy may have about IELE, because that may help you with the design of eWASM. Note that IELE was designed (and implemented) top-to-bottom using formal methods: the VM is generated automatically from its formal semantics in K, so it is supposedly correct by construction (supposing K is correct, of course, an argument which applies to all formal methods tools, including Coq, Isabelle, Agda).
Students in our team have started giving WASM a formal semantics in K more than two years ago (Daejun Park) and now have revived it (Everett Hildenbrandt), as you may know: https://github.com/kframework/wasm-semantics. So we are equally open to both WASM and LLVM. We chose LLVM mostly because LLVM was developed also in our department at UIUC, so we understand it well and like it and have tight connections with their team (and indeed, some of them provided significant help with IELE). Also, we already had a more complete K semantics of LLVM in K when we started than the WASM one, which turned out to be completely useless in the end.
Note that changes to LLVM were needed, which unfortunately resulted in not being able to use the LLVM optimizations and tool ecosystem "for free" as we initially hoped. We also had to give up some aspects of LLVM that were not really needed, thus only adding clutter and complexity. You should be aware of the fact that the same may happen with eWASM. I would not be too hopeful that you will get performance and portability "for free". In the end, I believe that eWASM will become a VM in itself, with its own tool ecosystem and evolution, without much to do with the original WASM. So I would only take from WASM what is conceptually nice and good, and not stick to it blindly. Just my 2c.