I'm really excited about the marriage of formal methods and practical application. I love to see this kind of cooperation between research and industry. At a minimum, the PL community's knowledge about formal specification should help the committee with its goal of making the spec clear and precise. We are actually hoping to see some correctness proofs as well--e.g., type and contract soundness. And I'm keeping my eyes peeled for other useful consistency properties worth verifying.
Sorry about the silence lately. Now that the word's out, I hope to talk more about some of the interesting points that come up in the EcmaScript process.