Technical Feasibility Study

In the first phase it is explored whether the technical implementation of this website, which intends to host course materials covering the foundations of computer science, is actually feasible. To determine feasibility, I explore several solutions for realizing these features:

• Explainer videos
• Interactive exercises

These two features are the minimum requirements. Although there are many other features that are desired in the final website (see also Ideas and Vision), by limiting the scope of features it will become possible to launch a Minimal Viable Product within a reasonably short time window.

Explainer videos

The first technical hurdle is the production of explainer videos.

Although I have tried different video editing software in the past, I found none of them easy enough to use. In particular, my workflow involves animating a lot of objects and doing so with high (algorithmic) precision: manual animation work is error-prone and too laborious.

In a previous project, where I wanted to visualize many different elements on the screen, I ultimately decided to programmatically generate the frames of the animation which were later composed using Blender. This was the result:

For the above video, I built the software that generated these animations from scratch (using Java and Java2D). Although not a bad result, the software I built in that case was specifically tailored to only produce the video above. Not much of it is easily reusable.

Hence I was looking for a different approach. Among the tools which can be used to make animated videos, I found the Manim project, that was started by Grant Sanderson, to be the best: it is easy to use, it scales well, and it has a beautiful aesthetic.

• The Manim project is more mature and more usable than my own software: Manim even produces MP4 files directly (in contrast to my own tool, which produced only sequences of images).
• Programmability of the animation tool is necessary for scalability and essentially reduces much of the animation work. Since the animations produced by Manim can be manipulated programmatically using Python, it becomes possible to simulate and visualize executions of complex algorithms.
• Finally, there are many interesting videos on the Web and on YouTube which are in the style of Manim: videos produced by Manim are immediately recognizable by their aesthetics alone.

Below is a proof of concept video that I produced, five months ago:

Interactive exercises

The next technical hurdle is implementing interactive exercises on the Web.

Four months ago, I created a prototype of an editor that runs in the browser that could be used as an input mechanism for interactive exercises on the Web. It relies on a back-end server for processing the commands received, and marks and disables editing the submitted entries. The user can also retract submitted commands, causing the text to become unmarked again. This allows the user to revise and resubmit new commands.

This attempt has two features: it makes use of the CodeMirror editor, and it clearly attempts to mimic how the Coq theorem prover works. While the user edits the commands and submits them to the server, a panel next to the editor can be updated to reflect the current state that commands influence. This panel could show different kinds of states: the state of a (partial) proof, the state of the execution of an algorithm, or the state of an entire simulated system. Presentation of these states could make use of anything available in the Web browser (text, vector or raster image, video, etc.).

However, implementing such a system costs a lot of time and effort. It may be better to reuse an existing tool that already works. One of those tools is jsCoq, which runs the Coq tool within the Web browser. Also jsCoq makes use of CodeMirror, but it also includes a version of Coq that runs on the client: no need to maintain a server back-end.

Here is a proof of concept:

Proposition test (A B: Prop): A \/ B -> ((A -> B) -> B).
  intro H.
  intro G.
  destruct H.
  - apply G in H. apply H.
  - apply H.
Qed.

The user can enable the Javascript port of Coq by pressing the power button on the right-hand side of the screen. A panel pops up which shows the state of Coq, and after loading the necessary resources, the user can step-by-step following along the proof.