“Look between the stars for what you need. The untraceable black of the possible…What does it mean to listen darkly?” (Healing Justice Lineages)

Other Formats

I gave a talk about Starling which you can watch on Vimeo.

The writing in this post is also available in a the format of a zine.

What is a Proof Assistant?

A proof assistant is a programming language and/or user interface that enables the creation of computer-aided proofs. Proof assistants are interactive theorem provers.

The subject of this article, Starling, is a proof assistant designed for ease of use by novices.

If this terminology confuses you, my expository talk might be helpful.

Why another proof assistant?

I was in a directed reading program for number theory which opened my eyes to the importance of proofs in mathematical discovery.

What do the proofs of the future look like? Can computer-aided proofs answer questions that pen-and-paper proofs are unable to answer?

Philosophy

I believe that new types of proofs make new kinds of knowledge possible.

For example, the invention of diagonalization proofs enabled a slew of monumental results in the 19th and 20th centuries such as Godel’s incompleteness theorem. Late in the twentieth century, a computer enabled the first ever proof of the four color theorem.

Will computer-aided proofs define the 21st century in the way that diagonalization proofs defined the 20th?

How does it work?

Starling can be seen as a surface language for the existing language Metamath. Starling compiles to Metamath, inheriting its library of verified proofs, as well as the Metamath proof verifier(s). Starling’s compiler is written in JavaScript.

Why Metamath?

I was particularly interested in Metamath because of its agnosticism toward different object logics. This enables you to write Metamath proofs whose theorems are derived from the axioms of quantum logic, for example.

Can I get involved?

I’m interested in designing this language to be as user-friendly as possible, so I am looking to interview people about their experiences using Starling. If that seems interesting to you, please talk to me!

Why even try something like this?

“If you find yourself inside a dimming world, remember it was always this dark inside the body.” (Ocean Vuong)

“The future is dark, which is the best thing the future can be, I think.” (Virginia Woolf)

---

How do you feel about proof assistants and formal verification? Share your thoughts in the comments :)