Proviola: A Tool for Proof Re-animation
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk

TL;DR
Proviola introduces a novel method for recording, replaying, and discussing proof interactions in formal proof systems, enhancing proof review and collaboration without requiring full proof assistant setups.
Contribution
The paper presents the proof movie concept, a new data structure, and a prototype implementation for proof interaction recording and replay, improving proof review and collaboration.
Findings
Proof movies enable proof review without full PA setup
The camera captures interactive sessions for replay and discussion
Movies facilitate collaborative proof analysis and annotation
Abstract
To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we in- troduce three related concepts, those of: a proof movie, consisting of frames which record both user input and the corresponding PA response; a camera, which films a user's interactive session with a PA as a movie; and a proviola, which replays a movie frame-by-frame to a third party. In this paper we describe the movie data structure and we discuss a proto- type implementation of the camera and proviola based on the ProofWeb system. ProofWeb uncouples the interaction with a PA via a web- interface (the client) from the actual PA that resides on the server. Our camera films a movie by "listening" to the ProofWeb communication. The first reason for developing movies is to uncouple the reviewing of a formal proof from the PA used to develop it: the movie concept…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Mathematics, Computing, and Information Processing · Open Education and E-Learning
