In section 19.3 of her book, Preece summarises [47] the four main classes of usability: learnability, throughput, flexibility and attitude. Interfaces such as Proof General are targeted primarily at throughput and flexibility. In many software systems the highest throughput of tasks is typically achieved by experienced users making use of the lowest level interfaces available. The vast majority of computer users don't care to deal with such details, preferring to sacrifice the raw throughput available to experts in favour of a less efficient solution that requires less effort from the user. The era in which computers were more costly than the salaries of their operators lapsed long ago. Therefore Igloo should be aimed at the easier end of the learnability scale, where user interfaces can be exploited to maximal benefit.
To be more explicit, we wish our user interface take less time to learn than existing proving interfaces. To achieve that, an ideal solution would remove the need for the user to learn about the internals of the proof engine and leave the user to operate with the more concrete concepts of the task at hand.
We also require that the interface be as flexible as possible, enforcing the benefits from the previous requirement. Given the choice between two simple programs that perform two slightly different tasks, and a single simple program that solves both situations, we prefer the latter.
It is also desirable that the user need not be required to learn a third party system unrelated to theorem proving before making it to the theorem proving itself. Examples of interfaces where this is not the case include the requirement of knowledge of Emacs when using Proof General, and the use of an X server on non-unix platforms when using interfaces such as XIsabelle and IsaWin.
|
|
|