4 ms·
There has been a WebAssembly interpreter implemented in Isabelle [1] and it's been proved correct. Not fast, but still pretty cool. [1] https://www.isa-afp.org
by titzer 8y ago
There has been a WebAssembly interpreter implemented in Isabelle [1] and it's been proved correct. Not fast, but still pretty cool.
[1] https://www.isa-afp.org/entries/WebAssembly.html https://www.isa-afp.org/entries/WebAssembly.html
- titzer 8y agoThat said, I still wouldn't put it in ring 0, as per my comment on the other thread: https://news.ycombinator.com/item?id=17186842 https://news.ycombinator.com/item?id=17186842
- monocasa 8y ago> Not fast That's the kicker. BPF is simpler, _and_ in spitting distance of native code perf. And if you're doing something crazy like injecting user code into interrupts, you care about perf. That being said, you're totally right that it's possible to get parity, just orders of magnitudes more work.