Building a Proof Assistant - Part I

I was still in the middle of my music undergraduate course when I took an interest in programming. Differently from what one might expect, it wasn't because I intended to study computer science for the sake of it and much less because I expected to make any money from that.

Since high school, I've always studied Maths for fun kinda like a side project if you will. One of the things that fascinated me the most about it, is how mathematical reasoning is purely deductive and each theorem is rigorously proved from previously established theorems, lemmas and definitions, recursively, all the way back to axioms.

Eventually, motivated by the desire to clarify hand-wavy arguments involving infinitesimals while studying calculus, I wanted to understand in greater detail how this deductive reasoning worked, what its rules are, what constitutes a rigorous proof and how to weave arguments in a precise manner. This led me to study logic.

Once I did that, I found exactly what I was looking for as formal logic gave me both a precise language with which I could formalize any Mathematical statement unambiguously and a proof system that had well defined inference rules that enabled me to write proofs that were guaranteed to be sound.

With these newly acquired tools, I would be able to (re-)build my mathematical knowledge upon solid footing, by formalizing theorems and proofs.

But alas, very soon I discovered that this is an exceptionally labour intensive task, which requires a lot of somewhat boring, repetitive work which also needed to be carried out meticulously as the tiniest mistake would render a whole proof, and all subsequent proofs that would depend on it, invalid.

And then it came to me: do you know "who" is really good with boring, repetitive work that needs to be done meticulously?

Computers.

So the next logical step in this formalization endeavor was to build a program to help me with that.

Turns out that this idea of having the computer aid us not only in writing and checking, but also discovering proofs is quite old. Programs that do such things are called proof assistants and automated theorem provers, respectively.

To be honest, this whole proof automation thing was never really my cup of tea. First and foremost because I was mainly interested in the formalization process as a way to deepen my understanding of mathematics and its proofs, and second because I didn't really believe that such an effort would be fruitful, although I do recognize that the recent advancements in AI research did change my opinion a little bit in that regard.

So with that said, I discovered that what I wanted to build was called a proof assistant, and that is what I set out to do.

Fast forward, I ended up learning C, then C++, and then JavaScript, the latter which ended up giving me a job.

In the meanwhile, I made many attempts at building a proof assistant, some of which where more successful than others, but none really came close to what I envisioned when I started this journey. This is partially due to the fact most of these attemps took place when I only knew C and C++, which although are up for the task, are definitely not the first choice when you're both learning how to program and trying to create a complex application. And then again, even when I eventually tried doing that with JavaScript, my lack of raw programming skills were a huge obstacle.

Now that I've been writing code for a living for quite some time now, I think it's a great time to try that again. I decided that I want to go all the way back to the very thing that sparked my interest in programming, and try to do it properly (as a toy project, of course, since I already have a job and do not want another).

So that's what I intend to do, for the forseeable future, whenever I feel like it and have some spare time, I'll be creating a proof assistant from scratch in TypeScript and documenting this process in this series.

Throught this process, we'll talk about logic, formal languages, mathematics, parsing techniques and programming in general, so if you are interested in any of these things, you'll probably enjoy it.