Bringing Theorem Proving to the (sonic) Masses

Emilio Jesús Gallego Arias (1) , Benoît Pin (1, 2) , Pierre Jouvelot (2, 1)

1 CRI - Centre de Recherche en Informatique
2 Mines Paris - PSL (École nationale supérieure des mines de Paris)

We explore the intersection of interactive theorem proving and digital signal processing through the use of web-based, rich interfaces. Traditionally, the barrier to entry to interactive theorem proving has been high. Provers are complex systems using obscure programming languages, and libraries may be underdocumented and use formalisms and notations far from the standard domain-specific practice. Thus, it doesn't come at a surprise that interactive theorem proving has seldom been explored in the the digital signal processing community. In previous work [1,2], we formalized several DSP tools and concepts using the Coq theorem prover [3]. [1] presents a simplified model Faust [4], a programming language tailored to audio DSP. The formalization allows to reason about Faust programs and prove typical properties like filter stability. In [2], we mechanized some theory of the Discrete Fourier Transform, following [5], and proving the main theorems. In our opinion, both developments are suitable as teaching material, either as an introduction to theorem proving or to students interested in DSP theory. However, in their current form, the student or reader must work with two versions of the document. The paper-and-ink version: which misses the interactive component of the theorem proving process, and the Coq proof scripts, that being plain text files usually miss convenient formatting and structure. This problem is also common in other teaching material (see for instance [6]), and while efforts to improve this situation have been made ([7] is one of the latest), the situation is still far from optimal, as most initiatives have been limited by implementation and platform choices. Our take on the problem --- inspired by the long tradition of interactive documents found in the computer music domain --- is to enrich the Coq document model to the full power of HTML5. Our goal is to have an integral solution, free of external components, so we have ported Coq to javascript, and we are writing a custom IDE for enriched proof documents. Thus, the once painful Coq installation and setup has become now a page load in the browser, document navigation and interaction can take advantage of browser support, and our documents can take advantage of most available JS libraries for extensibility. For instance, our model would allow to incorporate a javascript-based score like [8] and relate its output to a particular Coq datatype in a quite straightforward way. The primary design goal of the web-based user interface is supporting education and interactive papers, focusing on supporting excellent user feedback, comprehensive documentation search, and good notational/navigational facilities. The current prototype can be accessed at [9]. It supports full Coq functionality, but the user interface is still in heavy development. While support for the enriched document model won't likely be available at the time of this submission, the main technical difficulties of the development have been solved, thus we are confident on getting usable versions in the workshop timeframe.

Domaines: Son [cs.SD]; Traitement du signal et de l'image [eess.SP]

Emilio Jesús Gallego Arias, Benoît Pin, Pierre Jouvelot. Bringing Theorem Proving to the (sonic) Masses. 2015. ⟨hal-01254456⟩