The Twelf Wiki

Twelf is a programming language and theorem prover designed at Carnegie Mellon. As a college sophomore in 2003, I started working with Andrew Appel, among the first researchers to use Twelf outside of Carnegie Mellon. As I began my own undergraduate research with Twelf, I identified a need that was not met by the formal documentation and mailing list. People outside of the Carnegie Mellon needed more informal sources of introductions, tutorials, and intuition-building exercises.

In one form or another, I’ve been maintaining that resource for almost two decades!

Version 1: 2004-2006

With the encouragement of my undergraduate thesis advisor, David Walker, I petitioned Twelf co-author Frank Pfenning for space on one of his servers where I could manage a wiki resource using PmWiki.

Version 2: 2006-2024

When I started a doctoral program at Carnegie Mellon in the fall of 2006, a number of students in my research group were excited about growing the Twelf Wiki as a more complete resource. I used my school-provided desktop to run a MediaWiki instance for this more ambitious project.

I learned enough PHP to do a few customizations:

• The web server had an API endpoint that took Twelf code, ran it on the server, and returned Twelf’s response, along with a disk cache to avoid re-computation.
• A “Twelf Live” page provided an interface to this API endpoint, allowing anyone to use Twelf in the browser.
• A MediaWiki extension provided syntax highlighting and (using the aforementioned endpoint) the ability to show Twelf’s response to certain inputs inline on a page.

Thanks to the significant editorial contributions of a half dozen colleagues, the Twelf Wiki became a valuable resource. From September 2007 on, the wiki became twelf.org, the official home of the software.

Additionally, from 2006-2011 I hosted a nightly build process of Twelf that re-ran any changes against a large regression suite, approximating the modern best practice of continuous integration years before tools like Travis CI standardized open-source practices. (This same suite now runs as a GitHub action.)

Version 3: 2024-

I administered the Twelf Wiki without much fuss for longer than the company named “Twitter” existed. However, I was incurring ongoing hosting costs managing the cloud-based virtual machines that hosted Twelf, the outdated version of Mediawiki lacked some necessary tools for eliminating spam accounts, and the custom extensions made it difficult to upgrade Mediawiki.

In 2024, inspired by my spouse, Chris Martens, running a public course on Twelf, I transitioned twelf.org to its current form as an Starlight-generated static site with help from Jason Reed.

Meanwhile, Jason and Adam Goode did some compiler hacking to allow Twelf to run entirely in the browser. Utilizing their tool, I wrote a component that allows any piece of Twelf on the wiki to be opened in a browser-based editor along with its context.

The result is quite lovely: a modern website with rich content that invites interaction and learning, but with no analytics, no backend, and almost no JavaScript. It can easily take contributions through GitHub pull requests, and can be built locally by anyone with access to the git repository.