Some thoughts I want to share for the Coq track

If the Coq track isn't considered abandoned, I want to share some thoughts I have for the track.

Disclaimer

I consider myself a novice Coq user, but at least I've finished every standard and optional exercises in the first book of Software Foundations (SF), I'm active at StackOverflow mainly answering basic Coq questions, and most importantly, I've written some Coq challenges on Codewars (a kind of online judge site; my username there is "solitude").

Designing tasks for Coq track

Most exercises in common languages (say Python or JS) have this format:

Function skeleton is given. You need to write the function body, so that the function works as written in the description. The test file tests your function with various fixed inputs and checks the outputs against the expected values.

Coq can do much better; I can come up with at least four kinds of exercises (roughly ordered by increasing difficulty to write/solve):

Classic exercises (Write a function)

Same as the exercises in other languages. We can write a few exercises based on the common exercise pool. I say "a few" because Coq puts a hard requirement in the recursive nature of functions (in order to make them always terminate), which makes certain tasks much harder and sometimes impossible at all (e.g. Collatz).

Testing can be done with simple equality theorems.

Prove a given theorem

The most basic kind of Coq-specific exercise type.

A theorem without proof is given. You need to write the proof, so that the theorem is machine-checked as valid.

This is very similar to "Classic exercises" with "function" changed to "theorem" and "function body" to "proof". Canonical examples include a + 0 = a and a + b = b + a for natural numbers.

Testing can be done in two parts - testing the type of the theorem and checking that it does not assume any external axioms:

(* Exercise file: PlusCommutes.v *)
Theorem plus_commutes : forall a b : nat, a + b = b + a.
Proof. (* Correct proof *) Qed.

(* Test file: Tests.v *)
Require PlusCommutes.
Definition plus_commutes_test : forall a b : nat, a + b = b + a
  := PlusCommutes.plus_commutes.
Print Assumptions plus_commutes_test.

Write a function that satisfies a property

A function skeleton, associated with a set of properties it should meet, is given. You need to complete the function and prove that your function satisfies the given properties.

This is a (much) more sophisticated exercise type, as it requires you to complete a function and one or more theorems at once. It also often takes good mathematical/logical/domain-specific insights to complete.

For testing, you just test the theorems; you don't even need to test the function.

Formalize a property/relation and prove a theorem in the domain

An informal description of a property/relation is given. You need to write a formal definition of the property/relation and prove one or more theorems about it.

This is the most advanced exercise type (and the closest to how real researchers use Coq). Also, this is an exercise type that can't be fully machine-checked (as it involves the validity of an inductive definition), so it requires community/mentor review. This makes Exercism the best platform for them, as other online judge-style sites (including Codewars and Proving for Fun) can't hold challenges which can't be fully machine-checked. I guess this type fits best at the end of the core track.

In many cases, the theorem itself can be stated without the details of how a relation is defined, so we can still have a test file for some sanity check.

Structure and style of an exercise

Structure

Here are some examples of exercise structures out there:

My own works. I use _CoqProject to specify a prefix for the files in the same folder, and a Makefile generated using coq_makefile utility (the exact command can be found in makemake.sh). The test files themselves are from Software Foundations series.
Problem sets for Coq course at MIT. They use a stripped version of Makefile, and a pretty decent way to test an entire module. The usage of _CoqProject is the same.
Challenges on Codewars. Here we don't use any Makefile or _CoqProject (so there's no import prefix), and the command is just coqc Preloaded.v && coqc Solution.v && coqc Test.v where the three files contain definitions, exercises and test cases respectively.

If we have a way to set up make on Windows, it's probably best to use a Makefile. I guess three-file structure fits better than two-file because the preliminary definitions can be very long (up to ~100 lines depending on the task).

Coding style

AFAIK, Coq community doesn't have a consensus on coding styles, but here are some suggestions:

Filenames for Coq scripts should be an identifier, e.g. using hyphens is discouraged. Coq will emit warnings (if not errors) when you import a file whose name isn't an identifier.
There are several styles of filenames. The standard library and Software Foundations series use PascalCase. I've heard some projects use flatcase(?), that is, all lowercase and no separators at all. My personal preference is PascalCase.
Identifier names are split between PascalCase and snake_case. I don't think I've seen many camelCase. These are my personal preferences:
- Type names: still undecided between PascalCase and snake_case, but I like to use all lowercase for a single-word name, and PascalCase for multi-word / acronym-like names
- Constructor names: PascalCase
- Function, theorem, variable names: snake_case

Range of topics for core / side exercises

This is probably the hardest part of Coq track design.

Individual topics

Language features
- Basic functional programming (syntax, recursive functions)
- This part is pretty similar to that of Ocaml, with some restrictions.
- Dependent types (Vector)
- Basic theorem proving (tactics; rewrite, simpl, destruct, induction, some others)
Common concepts
- Logic (True, False, and, or, not, forall, exists)
- Polymorphism and inductive Props
- This involves dependent types under the hood, but (IMO) can be followed without full understanding of it.
Applications
- Mathematics
- Arithmetic
- Number theory (GCD, modular arithmetic, ...)
- Logic theory (classical logic axioms, ...)
- Set theory (cardinality, infinite sets, ...)
- Computability theory (halting problem, undecidable problems, ...)
- Programming languages
- Compilers, execution, compiler optimizations, type system, ...
- Correctness of algorithms
- Sorting, Fibonacci, ...

Core / side exercises

This is just a random list of ideas.

Core exercises could be split into two parts: introduction and application.
- Each core exercise at early stages should introduce a new topic to some depth, enough to move on to the next one. The volume of such an exercise could be (much) larger than those in other languages, probably up to (a fraction of) a small chapter of SF.
- They could also slightly (ab)use the mentoring feature, so that the exercises can leave some gaps (tactics?) and the students can research that part on their own or ask the mentor.
- Later ones could introduce some of the application areas.
The side exercises unlocked at early stages should not involve concepts not yet covered by core ones.
Basic topics are best covered using natural number arithmetic or list ops (as in SF), and inductive props can be introduced with a few applications.
- But there is evidence that some students are confused by the fact that they need induction to prove simple arithmetic properties. My idea is to use lists to introduce proof by induction, and then Peano arithmetic as an analogy (nil and cons correspond to zero and succ, respectively).

Another option is to simply assume that students have basic knowledge of syntax and concepts (e.g. picked up from SF), and directly dive into the fun with increasing complexity.

If you want, I can submit a pull request containing some exercises following the suggestions above. It might take days (or a couple of weeks) though.

exercism / coq