A lot of new stuff appeared yesterday on the Vdash home page. There is a very nice collection of links to information about formalized mathematics. The most interesting however is the roadmap page which states that Vdash will be based on ikiwiki wiki compiler and the monotone version control system. This represents a major shift in the concept.
Ikiwiki is a called a wiki compiler but really is more like a CMS integrated with version control. It can generate web sites from source files written in some markup language (most commonly Markdown). The web sites may support modifying through a browser (that is the defining feature of a wiki), or can look like a blog or just be a bunch of static pages that can be modified by commiting a change to the back-end version control system. Most websites powered by ikiwiki are not wikis. Visually they are rather simplistic. I don’t think displaying collapsible structured proofs is currently possible. There is a LaTeX plugin. Ikiwiki is written in Perl, but the plugins can be written in any language and communicate with the core via XML RPC.
Monotone is a distributed version control system. There is no central repository and each client can be a server as well. The clients talk to each other with a special protocol called netsync. Monotone has extensive hook and trigger facilities using lua. This was designed to trigger builds and testing as a reaction to commits, but of course in the Vdash context can be used to verify committed formal proofs.
The typical workflow for Vdash based on monotone would be as follows (from a post by hendrik on the Vdash mailing list):
Each mathematician has access to the repository. He uses it to check out theorems proofs, and theories, and writes new ones, using locally available software of his choice. Such software could of course also be part of the repository. When done to his satisfaction, possibly checked locally with his own version of the verifier, he checks in his new proofs.
So, the contributors will mostly work locally in their version of the repository. Monotone will provide the tools for sharing contributions, assuring consistency and accumulating the common knowledge.
Ikiwiki will be used as a way (possibly one of many) to create readable presentations and as an (probably rarely used) alternative way of modifying the repository.
This is of course my guess only.
Will it work? I really don’t know. This is very different from the obvious and known solutions, which may be both good and bad. It is definitely different than the Wikipedia concept. Wikipedia success was in large part due to lowering the barrier for users to contribute content. I don’t think requiring to use monotone does that for most people. On the other hand I personally would prefer to work this way than to struggle with a half-baked browser interface.
Maybe I should just stop speculating and wait patiently.