Structural editing (such as seen in the programming language Hazel https://hazel.org) is a powerful idea where the language is integrated with the editor, making it impossible to even *input* illegal programs. The work on the Graphical proof assistant Holbert is in a similar vein, where proofs are constructed interactively and an incorrect proof cannot be represented in the interface.
While Holbert 1 supported graphical rule editing and proof construction, the interface was unwieldy and more difficult than text editing. Holbert-ng, the upcoming version of Holbert being developed in ReScript with React, includes text-editing as a fallback option, and currently only has a rudimentary interface for interactive proof construction. This project would involve the design of a structural editor for proofs and inference rules in the Holbert proof assistant.
Experience in functional programming is useful, as the editor would need to be written in ReScript, a functional programming language. Experience in web programming (particularly React) would also be useful. Some understanding of proof assistants (e.g. Isabelle/HOL) is desirable but not required for this project.