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

TL;DR

This paper explores the use of focus groups to evaluate the usability of interactive theorem provers, highlighting adaptations needed for the ITP context and identifying usability issues.

Contribution

It demonstrates how focus groups can be adapted for ITP usability evaluation and discusses the impact of ITP characteristics on the evaluation process.

Findings

Identified usability issues in Isabelle/HOL and KeY systems.

Adapted focus group methodology for ITP context.

Provided insights into ITP usability challenges.

Abstract

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.