To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we introduce 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.\parIn this paper we describe the movie data structure and we discuss a prototype 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.\parThe first reason for developing movies is to uncouple the reviewing of a formal proof from the PA used to develop it: the movie concept enables users to discuss small code fragments without the need to install the PA or to load a whole library into it.\parOther advantages include the possibility to develop a separate commentary track to discuss or explain the PA interaction. We assert that a combined camera+proviola provides a generic layer between a client (user) and a server (PA). Finally we claim that movies are the right type of data to be stored in an encyclopedia of formalized mathematics, based on our experience in filming the Coq standard library.
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Roe, Kenneth; Smith, Scott: Coqpie: an IDE aimed at improving proof development productivity. (rough diamond) (2016)
- Kaliszyk, Cezary; Rabe, Florian: Towards knowledge management for HOL Light (2014)
- Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman: Communicating formal proofs: the case of Flyspeck (2013)
- Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman: Formal mathematics on display: a wiki for Flyspeck (2013)
- Tankink, Carst; Geuvers, Herman; Mckinna, James: Narrating formal proof (work in progress) (2012) ioport
- Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef: Large formal wikis: issues and solutions (2011)
- Wenzel, Makarius: Isabelle as document-oriented proof assistant (2011)
- Autexier, Serge (ed.); Calmet, Jacques (ed.); Delahaye, David (ed.); Ion, Patrick D. F. (ed.); Rideau, Laurence (ed.); Rioboo, Renaud (ed.); Sexton, Alan P. (ed.): Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5--10, 2010. Proceedings (2010)
- Tankink, Carst; Geuvers, Herman; Mckinna, James; Wiedijk, Freek: Proviola: A tool for proof re-animation (2010) ioport
- Tankink, Carst; Geuvers, Herman; McKinna, James; Wiedijk, Freek: Proviola: a tool for proof re-animation (2010)