A picture is worth a thousand words
A web page is worth a million!

Typical Coq Example

Lets add some math

JsCoq

Accessible Theorem Proving

Interactive Theorem Proving

Problems in Education

• 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 teaching books, but not runnable.
• Alternatives, like Edukera, either non-free, non realistic.

Interactive Theorem Proving

Problems with the Platforms

• Difficult to install, difficult to distribute. Very complex project!
• Highly non-standard protocols and formats.
• Reusability/modularity?
• Restricted to text ? Lack of hybrid document support.
• High abandonware ratio. Try to run a Coq development older than...
• Online tools that interface with a server: security hell, other problems (state, protocols, etc...)

JsCoq

A Serverless, Opinionated Project

Target a concrete user base, develop proper foundations.

HTML5:

• Write once, run anywhere, MOOCs.
• Decent math support, lots of libs.
• Future of UI, excellent support for interaction.

What we don't want to do:

1. Fork coq.
2. Invent anything.
3. Look like an IDE.
4. Write code. Write User Interfaces.

Yet we've done a bit of all of the above.

Demo Time !

Try it yourself!

• Demo I
• Demo II
• Demo III
• Demo IV

Many more developments supported, but they all (yet) look the same, we hope this changes!

We are Work-in-Progress™

How does it Work?

4 Modular Components:

The Coq Worker

Technology:

• Js_of_ocaml: Original project started as a JSOO test. Pushing the limits, or porting 300000 lines of Ocaml.
• Web Worker: We provide a generic Coq Web Worker that can be used by other projects.

Performance:

• Coq: Coq not very optimized for our enviroment, lack of profiling tools for Ocaml hurts.
• Perf Data: Size: ~3MiB, time to load, < 1 sec, libraries, between 3Mib and 300 MiB. Coq modules a "big" problem.
• Challenges: Actual results good. Remaining hotspots: Ocaml marshalling and jsoo/js tail call optimizations.

The Document Provider

Document Extraction:

• Code Providers: User-selected editor widgets, textareas, pre elements can form a stream of Coq sentences. May query the prover.
• CodeMirror: Our smart provider of choice. Key to success.

Document-Level Model:

• Provider Containers: Manage a set of Code Providers, focus, invalidation, next / previous.
• Delegation: Provider Containers talk to the manager on behalf of the providers.

The Document Manager

Responsible of the Prover-level Model.

• Main task: keep coherence between the two models.
• Written in ES2015 JavaScript, with minimal Ocaml help.
• Becomes thinner as we improve Coq's view of the world. Current size 500 JS lines approx.
• Should work with different providers/panels.

The Panel

• Prover-related UI (note the difference with code providers).
• Designed to wrap over an existing, generic document.
• Responsible to interpret "lateral" prover data, i.e. search results, configuration parameter, goals...
• Usually queries the prover for data.
• New panel in progress, using Jupyter JS UI.

What's Next:

SerAPI: @github

• New, highly flexible protocol; originating from jsCoq.
• Provides advanced access to Coq's internal, support for large scale development; working prototype.

Conclusions

• Quickly approaching an usable state.
• First 1.0 release expected soon.
• Already very useful, > 1000 users (ballpark estimate based on traffic, we don't track users).
• Interesting transfer of technology to the rest of the Coq ecosystem.

Open Source @ github.com/ejgallego/jscoq !

Hands-on-Session

• Explore SF (Beta Mode)
• Explore SF (Safe Mode)
• Go over the prime number proof.
• Try SerAPI
• Donwload a worker build!