How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of
Interactive Theorem Provers

Bernhard Beckert and Sarah Grebing and Florian Böhl


In recent years the effectiveness of interactive theorem provers has increased to an extent that
the bottleneck in the interactive process shifted to efficiency: while in principle large and
complex theorems are provable (effectiveness), it takes a lot of effort for the user interacting
with the system (lack of efficiency). We conducted focus groups to evaluate the usability of
Isabelle/HOL and the KeY system with two goals: (a) detect usability issues in the interaction
between interactive theorem provers and their user, and (b) analyze how evaluation and survey
methods commonly used in the area of human-computer interaction, such as focus groups and
co-operative evaluation, are applicable to the specific field of interactive theorem
proving (ITP).
In this paper, we report on our experience using the evaluation method focus groups and how we
adapted this method to ITP. We describe our results and conclusions mainly on the "meta-level,"
i.e., we focus on the impact that specific characteristics of ITPs have on the setup and the
results of focus groups. On the concrete level, we briefly summarise insights into the
usability of the ITPs used in our case study.