4 ms·
The SpecTec mentioned in the announcement is really cool. They're using a single source of truth to derive LaTeX, Sphinx docs, Coq definitions for proofs, and a
by pveierland 1y ago
The SpecTec mentioned in the announcement is really cool. They're using a single source of truth to derive LaTeX, Sphinx docs, Coq definitions for proofs, and an AST schema. Building the language spec in a way that its soundness can be proven and everything derived from one truth in this way seems super useful.
https://webassembly.org/news/2025-03-27-spectec/ https://webassembly.org/news/2025-03-27-spectec/