// HACKER NEWS — CYBERSECURITY
ExactTex. A gradually-typed superset of LaTeX
Know whether your document is sound before you look at the PDF.
ExactTeX is LaTeX with gradual annotation: you name the object you want checked, and what you do not name
stays ordinary LaTeX, transported byte for byte. Rename a .tex file to .xtex and it keeps working; from
there you choose how much to annotate, and what you annotate is guaranteed.
You can use ExactTeX in the browser today at Vitela —
an editor built on the compiler's WebAssembly build, with the same checks, diagnostics and navigation
running locally in the page.
Status: the compiler works, and three doors open into it. xtex parses, checks, emits LaTeX, writes
source maps and applies revisions; xtex-lsp gives an editor diagnostics, hover, completion and
go-to-definition; and the WebAssembly build runs the same core in any host with no compile server. A
parity suite holds the three doors to one answer. Every claim below is about what is built, and each
number is reproducible with the command that produced it.
Errors in your own words. When something does not fit on the page, LaTeX says:
Same fact, using the name you gave the object. This works only because you declared it — which is what the
syntax is for. It gives the tooling names to speak with.
Revisions that live in the file. Word stores tracked changes inside the .docx, which is why tools can
propose edits you accept or reject. LaTeX has no equivalent, so every tool builds its own layer and none of
them interoperate. ExactTeX puts the model in the format.
The file is ordinary LaTeX with one section annotated; the meter says how much of the document is
under contract. Now misspell the reference — change @ref(sec:results) to @ref(sec:resutls) —
and check again:
Plain LaTeX would have typeset that as a quiet ??. Requires a Rust toolchain
(1.88 or newer); the compiler itself has zero dependencies to fetch.
Two levels of annotation. @id(x) hangs off any LaTeX construct and buys checked references and safe rename
— theorems and algorithms work without ExactTeX knowing what they are. A typed block such as \figure(x)
also gives the compiler the fields to check: the image resolves, the caption is there, the column count
matches the tabular.