Demos

Best Current Demo

The engine browser carries 745 real Wikifunctions compositions, mechanically translated into F*, checked by F*, extracted to OCaml, compiled to JavaScript, and running in the page. Search by name or ZID, read each function as an s-expression, and run it.

This is the answer to: can we get JavaScript from complete composed Wikifunctions that bottom out in a checked primitive kernel? For 745 of them, yes, relative to the pinned local objects. 172 pass every Wikifunctions tester the project can read.

Each body also renders back to canonical Wikifunctions composition data, identically on round trip, so the F* form is convertible into wiki data rather than only derived from it.

Other Pages

• Z22294 focused demo: one composition end to end, in detail.
• Engine notes: what is generated, what is authored, and the measured numbers.
• Extracted F* playground (the earlier nine-function artifact): fixed examples, callable paths, JSON IR, and supported Z7 calls.
• Composition trees: local D3 graph browser for selected Wikifunctions trees.
• Extraction notes: commands and current limitations.
• Primitive grounding notes: what is grounded and what comes next.

Plain Terms

• F* is the checked source language used for the core definitions.
• OCaml is the extraction target produced from F*.
• js_of_ocaml turns OCaml bytecode into JavaScript.
• Z22294 and similar names are Wikifunctions object or function IDs.
• Z7 means a Wikifunctions function call object.