User Feedback

While the user interface is still in a developmental stage, informal user testing has confirmed a number of suspicions about the use of the interface:

• The need to understand Isabelle's data language, in order to specify theorems (see figure A.10) is by far the most restrictive feature of Igloo.

• It would be preferred that the theorem naming and theorem specification dialogs be merged into a single dialog, so that the mouse need only be used once.

• It would be preferred that the two most recent proof states be the ones that are automatically expanded as new proof states are created.

• Isabelle's non-English symbol syntax \ is confusing at first, and should make use of unicode (UTF-8) encoding where possible to render a more readable result.

Once Igloo stabilises some more, and additional features are added to PGIP, then formal user testing should be undertaken. This could include timing how long it takes new and expert Isabelle users to prove a series of increasingly complex proofs.