Require Import Coq.Strings.String. Open Scope string_scope. Definition hello:string := "Hello, World!". (* Unit test *) Lemma HelloTest: hello = "Hello, World!" . Proof. reflexivity. Qed.
What I like about it is that I am able to solve the challenges in a TDD way working in a environment that I am familiar (my own PC not a browser IDE) and the cherry on the top of the cake is that I have access to code reviews.
These are a few of the 3 exercises on the Coq track. You can see all the exercises here.