Apparaît dans la collection : MALINCA Kick-off meeting

Proof has a reputation for being hard to write and understand. What about the mediums for proof makes it so, and could we change it? In this talk, I share lessons learned from my group's work in the human-computer interaction (HCI) of proof and formalisms. I begin with a rich characterization of the modern UX of proof informed by a qualitative study of real work sessions of Rocq and Lean users. Then, I share ideas for how we might make proof more approachable, foregrounding my group's recent efforts to build tools that make notation more understandable and accelerate property-based testing. Along the way, I highlight strategies from our HCI work that have helped us gain insight into the realities of proof work and the effects of tools.