HenBlocks: Structured Editing for Coq
A block-based structured editor for the Coq Proof Assistant.
Visit HenBlocks
Introduction
HenBlocks is a web-based fully-fledged structured editor for Coq that I built using the Blockly library and jsCoq. The primary target audience for HenBlocks is undergraduate students who have some experience with functional programming but with little or no experience in proving. The intended use case is for such students to learn, discover, and practise proving with HenBlocks, and eventually transition to writing textual proofs in the Coq Proof Assistant via a text editor such as CoqIDE or Emacs.
HenBlocks was developed as part of my final year undergraduate Capstone project.
Achievements
I was invited to present HenBlocks at the Coq Workshop 2022.
I also presented HenBlocks at the International Conference on Functional Programming (ICFP) 2022 Student Research Competition and attained 1st place in the undergraduate category.