search

WebAssembly / multi-value

Proposal to add multi-values to WebAssembly
https://webassembly.github.io/multi-value/
Other
70 stars 24 forks source link

[spec] a better foundation for a mechanization? #23

Closed Huxpro closed 5 years ago

Huxpro commented 5 years ago

I am currently investigating a mechanized formalization (in Coq) on the setting of wasm spec instead of the PLDI formalization.

As I concerned in https://github.com/WebAssembly/spec/issues/1071, I found multi-value spec might be a better foundation of doing this work? My questions are:

  1. How big is the chance of this proposal making into the final spec? (which looks very promising to me).
  2. Has this fork caught up all the changes made into master?
rossberg commented 5 years ago

Great to hear that, I'm looking forward to it!

Yes, basing it on the multi-value proposal might be preferable. The proposal has been stable for a long time, there are no remaining concerns I'm aware of, and many other proposals depend on it. Its move to final adoption is merely awaiting a second production implementation to be completed.

I just rebased the repo on recent changes in upstream, so it is in sync.

Huxpro commented 4 years ago

@rossberg

I encountered some problems that get me stuck and they might be too irrelevant to post as a spec issue. Would you mind helping me out through email? I just reach out to your AT mpi-sws email address but not sure could that finds you well.

Thanks in advance!

conrad-watt commented 4 years ago

@Huxpro

Feel free to contact me too. I did the Isabelle mechanisation of the PLDI formalisation, so I might have some insight.

~As an aside, the PLDI paper already contained multi-value, so I agree that it's reasonable to mechanise~ (edit) but you already knew that

Huxpro commented 4 years ago

@conrad-watt Thxxx! Great to hear that! I have been aware of your pioneered work! (but was hesitate to dig into details due to my ignorance of Isabelle 😅)