djot.v: a verified djot parser, and a way to check syntax extensions

[hon-gyu]

Hi, I've written a djot implementation in Rocq, djot.v. Rocq is a dependently typed theorem prover. I used it to state djot's design goals as theorems and prove them. The main ones (from djot's rationale and the Beyond Markdown post):

• No backtracking: blocks are parsed line by line and a later line never changes an earlier block.
• Container uniformity: text in a block quote or a list parses as it would on its own.
• Local interpretation: whether [foo][bar] is a link does not depend on whether bar is defined.
• Safe hard-wrapping: hard-wrapping a paragraph should not lead to different interpretations.

The parser matches djot.js's test suite on all HTML cases.

What djot.v verifies is actually a family of syntax settings, and the official djot (specified by the syntax reference) is one setting of this family. Each setting comes with an answer to which of the properties above it keeps. The point is that extensions and dialects can be checked before they are adopted: either they keep every guarantee, or we know exactly which one they give up and can decide whether the tradeoff is worth it. For example, writing strong emphasis as ** instead of * keeps every property. Letting a list interrupt a paragraph, so a sublist no longer needs a blank line before it, costs safe hard-wrapping and nothing else.

I think many proposals for new syntax could be tested this way, in Rocq or any other prover. It would give us common ground for discussing which properties a proposal keeps and whether two extensions are compatible.

Rocq can extract programs to OCaml, Haskell and Scheme. The OCaml extraction is packaged as a library with a tuned API and has had performance work. The other two targets are possible but untested.

Gen-AI disclosure: most of the Rocq proofs were produced with a Gen-AI tool. The theorem statements are human-reviewed, and every proof is checked by Rocq with no axioms or admitted lemmas.

Edit 2026-10-05: I made a site that has a playground (with extension as checkboxes), the reference for the extensions, and the OCaml API docs.

[jgm]

Very interesting! I'd be curious about the performance of the Haskell program as compared to my own Haskell implementation, jgm/djoths.

[hon-gyu]

I did a simple benchmark. On a Macbook Pro with Apple Silicon with GHC 9.6.4 (-O2):

Details

Document	extracted Haskell with String	extracted Haskell with ByteString	djoths	djot.js	extracted OCaml (optimized)
empty (startup only)	16ms	17ms	17ms	64ms	3ms
readme.dj (12 KB)	20	20	21	74	8
readme.dj x16 (196 KB)	148	75	37	100	32
m.dj (243 KB)	180	109	50	112	47
m.dj x4 (974 KB)	709	321	126	198	136
m.dj x16 (3898 KB)	2734	1146	364	415	463
one line (75 KB)	53	249	26	96	27
one line (302 KB)	198	3341	78	162	79

All extractions pass djot.js's HTML rendering tests (287/287) while djoths does not (262/287).

In short, on large documents, Haskell extraction with ByteString about 3x slower than djoths and extraction with String is about 7x slower. ByteString goes quadratic on long lines, taking 13x the time for 4x the input.

The OCaml extraction has a few optimization. If all those tricks are ported to the Haskell extraction step, I estimate the performance will be around 1-1.5x slower than djoths.

[dereuromark]

Interesting.
I tried this out directly as a comparison tool also of MD vs Djot vs Carve.

I tried some combinations beyond the existing conformance cases and found a small footnote mismatch in the packaged OCaml parser at 3279f36:

[^n]: a
b

[^n]

Current djot.js (d93aff3) keeps both a and b in the footnote. Djot.v puts only a in the note and emits <p>b</p> in the main document.

The syntax reference explicitly allows lazy continuation of footnote paragraphs. Adding one space before b makes both parsers agree; adding a blank line before it also makes them agree, with b outside the note.

I packaged those controls and the failing cases in a four-case conformance fixture, with outputs and reproduction commands. The PFoot branch seems to close the note on an unindented line without checking for lazy paragraph continuation.

I also checked the failing block shape and the indented control directly in Rocq; both witnesses close without axioms. This looks like a useful case to add alongside the existing suite. It also illustrates a boundary of the current guarantees: passing the quote/list uniformity checks doesn't cover every container's continuation behavior.

[hon-gyu]

Thanks @dereuromark, this is a real missing point. I've added a new property about lazy line continuation.

djot.v did already have a uniformity theorem for footnotes. But something was missing in the shape of the input. The theorem statements did not say anything about a line that has no prefix (which could lazily continue a line). The footnote code was missing the lazy-continuation check. Quotes and lists happened to handle it correctly, but nothing proved that either.

The added missing theorem (a line that continues an open paragraph parses exactly as the same line with the containers' prefixes written out), together with the container uniformity, should now cover documents with lazy lines.