ff-html is a typed HTML library for building web documents from checked Agda data.
The library matters because it brings formalization into a familiar domain: web structure. It is not only about abstract proofs. It can render non-trivial HTML pages from typed Agda values, while tracking which tags, attributes, selectors, and style declarations are represented.
Coverage Snapshot
The safe specification represents all 115 active HTML element tags tracked in the MDN coverage work. It covers all 126 MDN attribute-table names through safe renderers and has renderers for every represented attribute key and value pattern.
The tracked safe surface includes:
- active element groups such as sectioning, text content, forms, media, tables, scripting, and web components;
- void/raw-text marker predicates;
- global attributes including
id, class, title, lang, dir, hidden, tabindex, data-*, aria-*, and role;
- structured token grammars for
rel, sandbox, and controlslist;
- typed inline style values through
ff-css;
- compatibility attributes such as
align, background, bgcolor, border, color, and summary with deliberately simple value languages.
Selectors And Stylesheets
The selector layer covers type selectors, universal selectors, ID/class selectors, attribute selectors, selector lists, and descendant, child, adjacent sibling, and subsequent sibling combinators. Static pseudo-classes such as :root, :first-child, :last-child, :only-child, and :empty are implemented generically.
The stylesheet layer connects ff-html selectors to ff-css declarations. It can render rules, track source order and specificity, and compute which declarations match each element. It is not yet a browser-computed cascade; inheritance, origin, importance, layers, media conditions, and conflict resolution remain future work.
Generated Examples
The generated pages are strong site artifacts:
- safe operations dashboard;
- component gallery;
- intro document;
- semantic article;
- selector/stylesheet example.
The safe dashboard shows a non-trivial page rendered from typed Safe HTML, with a coverage snapshot, request intake form, progressive controls, media, disclosure, and generated Agda provenance.
How It Fits
ff-html is one of the most visual libraries in the stack. It can show actual generated pages rather than only module names, especially when paired with ff-css.
Many formal artifacts are hard to show because they live in modules, proofs, and compiler output. HTML is different. A typed HTML tree can become a page that someone can open, inspect, and understand.
That makes ff-html a bridge between proof-assistant infrastructure and public-facing artifacts. Codex Scribe needs readable rulebooks and evidence packs. MLTTDB needs management surfaces for checked terms. State Machine Studio needs generated views and previews that stay close to formal representations.
The careful boundary is equally important. ff-html is a typed document, attribute, selector, and stylesheet-matching layer. It is not a full browser model. That scope is the right fit for generated artifacts that need to remain close to checked data.
