When writing a computer program, we often use unit tests to check correctness. However, unit testing is insufficient to detect all errors, resulting in the potential for software bugs. A better way to demonstrate correctness is to use proofs to guarantee that our program is bug-free. One popular way of writing proofs is using the Coq Proof Assistant. However, there are a number of pain points in using it, which affects beginners most.

Structured editors, which allow the user to manipulate structured blocks corresponding to the abstract syntax of a program, have been used to make programming more accessible to beginners. However, they have not been applied to proving thus far.

The objective of this capstone is to build an interactive graphical user interface for the structured editing of Coq proofs. In this thesis, we present HenBlocks (available at https://henblocks.github.io), a web-based fully-fledged structured editor that allows users to write Coq proofs by manipulating blocks. We conclude that structured editing is a promising approach to proof writing that warrants more exploration, development, and testing.