2 ms·

Nice find. Still, look to be interpreted though. It gets JIT compiled to native code that runs (for some code shapes yadda yadda usual story) about 10% slower

Nice find. Still, look to be interpreted though. It gets JIT compiled to native code that runs (for some code shapes yadda yadda usual story) about 10% slower than gcc, if I recall correctly. Without the safety aspect it can run as fast as GCC for some benchmarks. As I linked in my other comment, WASM was built with mechanized proofs nearly from the outset. They learned from the mistakes made in the CLR and JVM. But so did the CLR and JVM designers. The paper you link to says the hard part of JVM bytecode verification is the jsr "subroutine" control flow instruction. This instruction has been phased out, bytecode version 51+ doesn't allow it anymore. Whilst a JVM may well support verification of older bytecode formats, and that verification is still safe and sound, you can implement the latest version of the spec and avoid that entire design error. Given that, and given that the JVM type system has been proven sound despite being significantly more powerful than WASM's, I'm not really certain how this is meant to prove that WASM is better.

naasking 8y ago
> But so did the CLR and JVM designers. No they weren't. Formalization and verification of the IR came much later in both cases. > Given that, and given that the JVM type system has been proven sound despite being significantly more powerful than WASM's, I'm not really certain how this is meant to prove that WASM is better. "Significantly more powerful" is way overstating the case. In fact, I'd hazard that it's flat out wrong. You can easily express some patterns in JVM bytecode, but other patterns not at all. Secondly, WASM's primitives types are much more flexible than those available on the JVM. For instance, unsigned types. Finally, the JVM carries a lot of baggage, a) in terms of backwards compatibility as you briefly mention, b) in terms of unnecessary control flow instructions which unnecessarily complicate verification (like exceptions), c) unconfigurable runtime that's poorly suited to some programs, d) an overly complicated security model that's an impediment more than a help, etc. I could probably come up with a dozen more reasons, but that's just off the top of my head.

naasking 8y ago

> But so did the CLR and JVM designers. No they weren't. Formalization and verification of the IR came much later in both cases. > Given that, and given that the JVM type system has been proven sound despite being significantly more powerful than WASM's, I'm not really certain how this is meant to prove that WASM is better. "Significantly more powerful" is way overstating the case. In fact, I'd hazard that it's flat out wrong. You can easily express some patterns in JVM bytecode, but other patterns not at all. Secondly, WASM's primitives types are much more flexible than those available on the JVM. For instance, unsigned types. Finally, the JVM carries a lot of baggage, a) in terms of backwards compatibility as you briefly mention, b) in terms of unnecessary control flow instructions which unnecessarily complicate verification (like exceptions), c) unconfigurable runtime that's poorly suited to some programs, d) an overly complicated security model that's an impediment more than a help, etc. I could probably come up with a dozen more reasons, but that's just off the top of my head.