主要观点：两周前 Wasm 社区组投票采用 SpecTec 用于编写未来的 Wasm 规范，本文介绍了 SpecTec 的相关内容及意义。
关键信息：

• Wasm 与其他主流编程技术不同，有完整的形式化定义，其规范包含形式化和自然语言版本，二者相互补充但增加了作者和编辑的工作负担。
• SpecTec 是一种领域特定语言，可忠实表达 Wasm 的形式规则，生成多种输出，如带交叉引用的 LaTeX、Sphinx 标记的英语散文、Coq 证明助手的定义、可被其他工具消费的机器可读 AST 等。
• SpecTec 能通过元解释器执行生成的散文以验证其正确性，还能为 Coq 生成定义以证明语言的完备性，近期开始为 SpecTec 开发生成.wast测试文件的后端，可提高实现的保证水平。
• 现在 CG 已投票采用 SpecTec，正在解决渲染问题，之后将其合并到主 Wasm 规范仓库，Wasm 2.0 和当前提案已集成到 SpecTec 中，官方 Wasm 3.0 规范也将用 SpecTec 生成。
  重要细节：
• 1990 年《The Definition of Standard ML》出版，是通用编程语言的第一个综合形式定义。
• Wasm 规范的形式化版本在自然语言版本之前编写，二者编写过程都很繁琐且易出错。
• WasmCert 维护 Wasm 的机械完备性证明等工作，与 Wasm 的发展节奏存在挑战。
• SpecTec 的实现是有多个内部表示和后端的编译管道，能从形式规范生成多种输出并提供新的保证水平。
• SpecTec 不是 AI，是精心设计的翻译过程，追求准确性和严谨性。