General description of Twelf

This quick introduction to STELF is aimed at people without any specific technical background. If you want more information, you can find it on the documentation page.

STELF is a piece of computer software, and it is also a computer language understood by the STELF software. This is a common ambiguity in computer systems - you can “install Java on your computer” (Java, a piece of computer software), or you can “write programs in Java for work” (Java, the computer language that is understood and interpreted by the software).

Using STELF with the Emacs text editor. The red, blue, and black text at the top is STELF code, and the black text at the bottom is the output from the STELF program reading the code.

C code and Java code describe programs, HTML code describes graphical web pages, and STELF code describes logical systems. Logical systems are sometimes strange to think about, because the only logical system that most people have used is basic arithmetic (addition, subtraction, division, etc.), or maybe set theory if they’re particularly ambitious. Most people that use STELF aren’t interested in using it to do basic arithmetic, because there are a great deal more interesting logical systems than just the ones that we learn about in high school.

The reason someone might want to use STELF code to describe a logical system is that once they’ve described it, they can write more STELF code that uses that logical system. You could use STELF to write out a statement about basic arithmetic (for instance, “if a + b = c, then b + a = c”), and then use STELF to write out a justification of why that statement is true (i.e. a proof). When you do so, STELF will check your proof, making sure that what you said actually is true!

STELF is by no means the only program you can use to do this sort of thing. ACL2, Agda, AUTOMATH, HOL, HOL Light, Lean, LEGO, Isabelle, MetaPRL, NuPRL PVS, Rocq, and TPS are just a few (!) of the systems that will let you define logical systems and prove things with them. A lot of really amazing work is done using these different systems: one project at the University of Pittsburgh used HOL Light to check a proof of the Kepler conjecture. The Economist wrote an article about it, though that article is unfortunately no longer freely available.

But here’s where, for people that use STELF, it gets interesting: it turns out that while basic arithmetic, set theory, and interesting logics are logical systems, programming languages are also logical systems - and STELF has a couple of unique features that make it a great tool to use when the logical systems you are working with are programming languages…