Bringing Theorem Proving to the (sonic) Masses
Emilio J. Gallego Arias, Benoit Pin, Pierre Jouvelot
MINES ParisTech, PSL Research University, France
3 Novembre 2015  CIEREC SaintEtienne
Des outils et des méthodes innovantes pour
l’enseignement de la musique et du traitement du signal
Theorem Proving
$\cap$
Signal Processing =
?
Potential of Combining Topics?
JsCoq
Accessible Theorem Proving
Interactive Theorem Proving
Some Current Problems

Hard, awkward interfaces and platforms (emacs).

Not the most appealing to students, low coolness factor.

Easy accessibility is crucial to learning; we learn to prove
and program by imitation.
"The Youtube Epoch"

Get the proofs out of their hole! Ubiquity.

Long tradition in literate or "embedded" teaching books, but not runnable.

Alternatives, like Edukera, nonfree, non realistic.
Signal Processing:
Underexplored Area in ITP!

Provides interesting, small but not trivial examples.

Sound processing has high coolness factor.

Future of math proofs and exercises want to be computer checked.

"Experts" in DSP can really benefit from some education in
ITP, but we need to lower the barrier to entry.

Formal considerations at the Faust designlevel.
The Platform
HTML5
 Write once, run anywhere, MOOCs.
 Decent math support.

Excellent support for interactivity.
Coq
 Industrialstrength, mature theorem prover.
 Standard in the domain, many highprofile users.
 Extreme demand for experts.
Coq: Some Facts
 Functional programming language.
 Provides very strong evindence, minimal kernel.
 Programs are proofs types are specifications.
 Strong automation.
 Particularly wellsuited for algebra, program verification.
A Typical Theorem:
$$ \mathsf{Thm1} : \mathsf{Hyp1} \to \ldots \to \mathsf{HypN} \to \mathsf{Concl} $$
Coq: An Example
"Alt→": Coq's panel; "AltEnter" go to point; "AltN/P": Navigate.
Rewrite/Equality
$$ n + m = m + n $$
Another very important tool: big operators!
$$ \sum_i^N F(i) \qquad \ldots \qquad \prod_j^N F(j)$$
$$ \sum_{i = m + a}^{n1} F(i) + \sum_{i = m}^{(na)1)} F(i)$$
Demo I:
Discrete Fourier Transform
 The DFT with MathBox (by Kevin Reid).
 DFT in Coq/MathComp.
JsCoq Architecture
Two Layers

Providers:
Editor widgets, textareas, pre/elements; they provide the
next piece of code, invalidate old ones...

Manager:
Manages a set of providers that constitute a document.
Modularity

We expect to use the same framework for other kind of
interactive programs, i.e.: Faust. or provers: Lean.
Conclusions
 Still pretty much a technology demo, but quickly
approaching to a usable state.
 Public alpha release soon, already gathered some interest
and positive feedback from Coq community.
 Size/Time: 5 MiB (4 sec), Libs, 10  100 MiB (< 20 secs)
 Works in progress:
introduction to Coq, several interactive blog posts, DFT
tutorial, Mini Faust tutorial, port of "Software Foundations".
Open source project at
github.com/ejgallego/jscoq
/