wikifn-fstar

Wikifn Engine Browser

3,893 real Wikifunctions compositions, mechanically translated into F*, checked by F*, extracted to OCaml, compiled to JavaScript, and running in this page. Search for a function, read its source as an s-expression, and run it.

Not all of them can run yet, and there are two different reasons. A function is runnable when every function it reaches is implemented; the rest are carried because calls are by reference, so they start working as soon as the gap is filled. Separately, some reach compositions defined in terms of each other with no base case: those cannot return an answer however long they run, and are marked like this rather than left for you to discover.

What still fails — every Wikifunctions tester run against this engine, grouped by cause.

The same engine runs outside the browser. From a clone: node examples/node-engine.js Z10627 "Hello, Wikifunctions!" calls one function and prints its signature, its source and its answer; node examples/compose.js feeds one function into another. Calling it from JavaScript has the full instructions.

Demos menu · How it works

Loading the engine

The artifact and catalogue are a couple of megabytes, served compressed. They start downloading as soon as you arrive; nothing can be searched or run until they finish, and the status below says which it is.

Starting…

Browse and run

Search runnable only

Select a function

Source

The composition, printed as an s-expression by Wikifn.Print — the same checked F* module the evaluator uses, so the two cannot drift. Names are the ZID followed by the English label, so the text reads as language while still mapping back to identifiers. Primitives that LISP already named keep the classical name.

What this is and is not

Each body is a mechanical translation of a pinned Z14K2 composition. None of it was written by hand, and each carries the revision and digest it came from.
The primitives underneath are written by hand, in F*. They are a claim about what Wikifunctions means, checked against Wikifunctions' own testers rather than proved.
A function marked runnable has every function it reaches implemented. Being runnable is not the same as being verified: only the tester results in the engine notes support correctness claims.
Arguments are literal values. There is no object store, so a reference is refused rather than read as text.
Some compositions are defined in terms of each other with no base case. Z844 boolean equality is not(inequality) while inequality is not(equality); reversing a list is defined through appending to one, which is defined through reversing. Where another implementation escapes the cycle the generator picks it, and where the wiki's own evaluator escapes by preferring a code implementation the function is grounded in the kernel instead. What is left reports a depth limit rather than returning an answer.
Each function shows its declared argument and return types. Those come from the pinned Z8 and are not checked: the engine has no type checker, so they say what the function was declared to want, not what it enforces.
Fuel is a budget for total evaluation steps, not a depth limit. Running out is reported, not hidden. Naively recursive functions can need a lot: the corpus's Fibonacci needs about 200,000 steps for n = 20, because it is written without memoisation.

Downloads: catalogue, everything as one loadable Scheme file, the definitions alone, the prelude alone, name hints, all back as canonical Wikifunctions compositions.