Writing vowsite in Vow

The documentation and examples were enough to write this program without reading the compiler's generated C. Verification was smoother than writing a correct Markdown parser: the first version verified, but a later test exposed incorrect inline rendering. This report distinguishes those two kinds of correctness.

Numbers

Friction log

Times are approximate, reconstructed from the working notes below.

  1. The standard library is very small (roughly 3 minutes of design). There is no string split, substring search, prefix test, trim, or directory creation. I expected to need parser helpers, but a sizeable part of the program is basic text plumbing. There was no diagnostic: I checked the documented built-ins first. I wrote bounded pure helpers, retained original line endings in a Line struct, and made the shell/Makefile create output directories.

  2. The subset did not directly fit the source documents (about 3 minutes). Browser inspection showed list continuation text outside its list item, and the README's indented fence was rendered as paragraph text. I had expected copying the documents and fixing links to be enough. The task's flat lists and column-zero fences do not cover that formatting. I reflowed list items, unindented the copied fence, and removed blockquote markers in site/ only. No compiler diagnostic; original documents remain unchanged.

  3. The first delimiter search was incorrect (about 2 minutes). A newly added nested-inline fixture produced this diff:

    -<p><em>Emphasis with <strong>strong</strong> inside</em>.
+<p><em>Emphasis with </em><em>strong</em><em> inside</em>.

    make reported make: *** [test-site] Error 1. A double star inside inline code also closed an outer strong span prematurely. I expected nested markup and code spans to retain their boundaries. The fix was emphasis_end, which skips code spans and searches nested delimiters with a proved shrinking suffix. The expanded fixture now passes. This was my parser bug; verification had correctly proved bounds and termination, not Markdown semantics.

  4. Test summary count (less than a minute). The initial shell message said 14 integration checks passed, although there were 13. I counted the six successful rendering/manifest cases, six failure cases, and empty-manifest case, then corrected the message. All checks themselves had passed.

  5. Browser tooling (about a minute). Browser discovery returned No browser is available. Native Chrome was available through computer use, so I used that to inspect the generated files. I checked all four required pages, including the corrected lists, code examples, and specification table.

  6. Optional performance measurement (less than a minute). macOS time -l reported time: sysctl kern.clockrate: Operation not permitted. Site generation itself succeeded. I did not pursue an unnecessary permission change and make no reliable timing or peak-memory claim here.

Documentation gaps

I found no statement in VOW_FOR_LLMS.md that I could demonstrate was wrong. The most useful instructions were the explanations of loop havoc, callee contracts, expression predicates, and non-mixed binary operators.

Concrete additions that would have helped:

The guide's while more example intentionally has no measure. It is valid Vow, but not a pattern one can copy unchanged into this task, which requires total termination proofs. This is a distinction to highlight, not a compiler defect.

Verification experience

Easy: the escaper's quantified tag_free(result) postcondition and loop invariant worked using the technique from examples/escape.vow. Range loops supplied indexing bounds; string bytes were accepted by char. find and link_end return contracts made subsequent slices straightforward.

Most reasoning before compilation: nested block loops. The renderer consumes at least one line before entering each inner loop, saves that position as start, and preserves start <= i <= len(src). Thus the outer loop still knows it progressed, including when an inner list/table loop breaks. The two recursive inline helpers use len(s) and len(s) - start as their measures. Each recursive call sees a strictly shorter input or remaining suffix.

No required proof was abandoned, weakened into check, or bypassed. There were no failed proof obligations, solver timeouts, or counterexamples, so I cannot claim counterexamples helped in this session. The deliberate bounds/progress structure probably accounts for the lack of solver friction.

The proved property of escape is specifically absence of literal angle brackets. Fixtures additionally check escaping of ampersands and double quotes. I did not formally prove the whole renderer equivalent to a Markdown grammar, that URLs use safe schemes, or that every generated HTML fragment is balanced. Those properties received runtime tests and an independent HTML audit instead.

Language assessment

Named arguments helped with functions carrying several positions and strings. Pure-by-default functions made the I/O boundary obvious. Explicit contracts on search helpers were useful design constraints, not just proof annotations. Labelled ends made the deeply nested parser unambiguous.

The cost was verbosity. No precedence demands many parentheses in simple bounds tests. No shadowing requires distinct names throughout nested control flow. A Boolean prefix helper does not automatically expose its internal bounds facts, so I used explicit guards where a later slice needs them. This is consistent with signature-only reasoning, but a less repetitive predicate-contract idiom would help. I missed ordinary string utilities, a string builder with verification support, filesystem directory creation, and structured I/O error information.

Most output uses lists of fragments and join, following the guide. The proved escaper retains the example's repeated concatenation. Consequently, a single very long escaped span can have quadratic copying/allocation cost. The runtime does not reclaim memory, and recursive inline parsing also consumes stack. This is a batch documentation generator, not a bounded-memory streaming parser. Termination proofs alone do not establish resource limits.

The implementation deliberately remains a Markdown subset: flat lists, no raw HTML, no backslash-escape or complete CommonMark delimiter/flanking algorithm, and no table alignment syntax. It preserves UTF-8 bytes, code line endings, and missing final newlines. Invalid/missing input and failed output writes are tested; generation is not transactional if an I/O error occurs after an earlier page was written. The site template is trusted markup; Markdown and titles are escaped.

Compiler bugs and reproductions

No compiler or runtime bug was found. There is no minimal compiler-bug reproduction to provide. The nested-inline fixture above is a minimal regression for my own parser mistake. I did not read seed/vowc.c, and did not modify the compiler, runtime, original README, or docs/.

Final validation

Notes recorded during implementation