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 Saint-Etienne
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, non-free, non realistic.
Signal Processing:
Under-explored 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 design-level.
The Platform
HTML5
- Write once, run anywhere, MOOCs.
- Decent math support.
-
Excellent support for interactivity.
Coq
- Industrial-strength, mature theorem prover.
- Standard in the domain, many high-profile 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 well-suited 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; "Alt-Enter" go to point; "Alt-N/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}^{n-1} F(i) + \sum_{i = m}^{(n-a)-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
/
