A Distributed and Trusted Web of Formal Proofs - Archive ouverte HAL Access content directly
Conference Papers Year : 2020

A Distributed and Trusted Web of Formal Proofs



Most computer checked proofs are tied to the particular technology of a prover's software. While sharing results between proof assistants is a recognized and desirable goal, the current organization of theorem proving tools makes such sharing an exception instead of the rule. In this talk, I argue that we need to turn the current architecture of proof assistants and formal proofs inside-out. That is, instead of having a few mature theorem provers include within them their formally checked theorems and proofs, I propose that proof assistants should sit on the edge of a web of formal proofs and that proof assistant should be exporting their proofs so that they can exist independently of any theorem prover. While it is necessary to maintain the dependencies between definitions, theories, and theorems, no explicit library structure should be imposed on this web of formal proofs. Thus a theorem and its proofs should not necessarily be located at a particular URL or within a particular prover's library. While the world of symbolic logic and proof theory certainly allows for proofs to be seen as global and permanent objects, there is a lot of research and engineering work that is needed to make this possible. I describe some of the required research and development that must be done to achieve this goal.
Fichier principal
Vignette du fichier
icdcit-2020.pdf (255.59 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-02468229 , version 1 (05-02-2020)



Dale Miller. A Distributed and Trusted Web of Formal Proofs. ICDCIT 2020 - 16th International Conference on Distributed Computing and Internet Technology, Jan 2020, Bhubaneswar, India. pp.21-40, ⟨10.1007/978-3-030-36987-3_2⟩. ⟨hal-02468229⟩
221 View
228 Download



Gmail Facebook Twitter LinkedIn More