About

My background is in C/C++ software development with the occasional dabbling in other OOP languages like Java. Before learning Coq, I had minimal exposure to functional programming. Math-wise, I took in Calculus college, then forgot most of it.

With programming, I love the interaction with the computer. You writes some code, tries to run it, and bam the computer says there is a syntax error. You fix the syntax error, try to run it, then boom it crashes. Although that interaction may sound unpleasant, I find it much more reassuring than writing a math proof on a piece of paper.

Informal math proofs are not checked by a computer. Along with that freedom comes the ambiguity. Often when I read someone else's informal proof, I feel like the preposition they are trying to prove is correct, but their proof doesn't show it.

If I write an informal proof, it just sits there on a piece of paper. Nothing validates the proof unless it is submitted to a peer review process.

Philosophically, I feel like learning math should be an interactive process like computer programming. I started searching for an answer, and I found Coq.

Coq is extremely powerful, although with awkward syntax at times. There is still much active development in Coq's foundations, but I think Coq's biggest weakness at this point is documentation. See this message from the mailing list for another person's experience with this.

This blog is about making Coq more accessible. This blog especially focuses on learning math through Coq (instead of figuring out how to apply math you already know in Coq).

It seems that most documentation for Coq comes in the form of books. Books are great, but as part of making Coq more interactive, I decided that a blog is more interactive, and it has a lower barrier to entry.

This blog is a work in-progress as I learn more about Coq and math myself. Comments are always welcome.