I successfully defended my Computer Science PhD dissertation at the University of Iowa in 2014. As a PhD student, I worked on the human-computer interaction problem of finding ways to make complex tasks like math and programming easier to do and learn. I aimed my work at several big issues:
I worked on two distinct projects in my research: Keyboard-Card Menus and user interfaces for the Coq Proof Assistant. However, in my dissertation (and in the second video below), I demonstrated how the former may be applied to the latter.
Keyboard-Card Menus were a method I developed for helping users learn shortcuts quickly. I presented these, and a study demonstrating their effectiveness, at the Interaccion Spanish HCI conference in 2013.
One of my hopes is that this sort of system could be used for entering and manipulating math. LaTeX can be used to create nicely typeset equations, but I do not think it is fast enough to learn or to use:
\frac{}{}" starts to seem slow and awkward when one compares it to drawing a short line on a piece of paper. This might not be the case if we can reduce the number of keystrokes from 9+ down to, say, 2.Below is a prototype for a structure editor that uses keyboard-card menus and syntax tree highlighting in the jEdit plugin. This particular setup is for doing Fitch-style natural deduction Coq-checkable propositional logic proofs, but I imagine you could use similar techniques to write and edit HTML, XML, LaTeX, Java, etc...the idea is to make it faster to write syntactically correct documents. A few things to note:
Coq is one of the most powerful and widely used interactive theorem provers. It is really a tool that helps you to create programs in a language that has a very sophisticated type system. The type system is actually so sophisticated that (1) types can be used to state mathematical theorems, (2) a “term” (e.g. a function) can be viewed as a proof of its type, and (3) type-checking can be viewed as proof-checking. All of this gets to be very complicated, which why I worked on new user interfaces to help people use the tool.
I developed a jEdit plugin, tentatively called CoqEdit, that serves as a new, experimental user interface. The basic version is similar to CoqIDE (which comes bundled with Coq) and Proof General (an Emacs mode that is used with several other interactive theorem provers as well).
The videos above show a potential CoqEdit add-on that I had students at the University of Iowa try out as part of a usability experiment. The video below is actually a tutorial on proofs, and how to do them with CoqEdit, that was used in the usability experiment; if you just want to see how the user interface works, I would skip ahead to 4 minutes 50 seconds and watch the next three minutes or so (maybe on 2x speed).
I also developed an additional jEdit plugin, called "Proof Previews"" that can be used with CoqEdit to provide a pop-up completion menu of available commands (i.e. restricted to commands that do not immediately produce errors) and allows users to preview the effects of entering the selected command before it is actually entered.