Lab Lunch: 23 March 2021 - Paul Jackson

Title:  Dynamic Proof Presentation

Abstract:

Over several decades there has been significant debate about the style of formal proofs supported by proof assistants such as Isabelle, Coq and Agda.  For example, the merits of a declarative style rather than a procedural (tactic) style have been argued.  In much of the debate there has been unnecessarily-rigid insistence on the languages of proof input and proof presentation being identified.

This talk is a overview of the opportunities opened up when these concepts are not shackled together, when proof presentation is a dynamic activity that  takes full advantage of the capabilites of computer user interfaces.  For example, with dynamic proof presentation, the proof viewer can easily focus  attention on particular parts of proofs and change the level of detail presented. One viewer might be interested in just a proof outline, another might want to see how a large step of inference is composed of smaller steps.

Current proof assistant user interfaces do provide some dynamic presentation capabilities, but much more could be done.  Further attention to dynamic  proof presentation should help make formal proofs easier to understand by a wider range of audiences, without the need to rewrite proof libraries that are  developed with huge time investments.