Formal methods in robot end user development: progress, gaps, and opportunities

End user development (EUD) is an emerging paradigm in human–robot interaction, involving end users both creating and maintaining robot programs themselves. Formal methods encompass a set of techniques that are useful to EUD, emphasizing the correctness of programs that are often created using natural, on-the-fly and sometimes even sloppy end-user input. These techniques include, for example, correct-by-construction synthesis of robot programs given incomplete developer input, automated repair of these applications and formal verification of these applications against sets of correctness criteria. Despite the increasing popularity of EUD and formal methods individually in robotics, there is no comprehensive review of how both have been successfully combined. The primary objective is thereby to review current practices for applying formal methods within robot EUD. To achieve this objective, the authors include adjacent areas of EUD research, such as natural language programming, and adjacent approaches to formal methods, such as automated planning. Recognizing that the integration of EUD and formal methods in robotics is still a nascent topic, the secondary objective is to identify opportunities for future research. This review thereby provides a primer on how to conduct further integration of formal methods in robot EUD.