It’s been close to a year since Coq support was first added to Codewars and I am excited to announce that Coq support is now officially stable! 
Many thanks to all of you who have joined Codewars since my last invitation, especially those who have participated in the Beta Process by completing Coq challenges in Beta and leaving your satisfaction + ranking votes on them which was extremely crucial in getting them approved. In particular, I would like to thank @JasonGross for his exceptional contribution by authoring 3 of his own Coq challenges on our platform (2 of which have been since approved) and participating in the final re-rankings which enabled Coq support on Codewars to finally leave Beta.
For those of you new to Codewars, I hereby invite you to sign up for an account. Codewars is a training platform where programmers of all disciplines train on code challenges called Kata in order to improve their programming skills. For Coq, we currently boast 74 Kata (54 approved, 20 in Beta) spanning topics on discrete mathematics, mathematical logic, verified functional algorithms, programming language theory and more, so I’m sure you will be able to find Coq challenges to your liking whether you are a computer science undergraduate just getting started with Coq or a programming language researcher working at one of the world’s top universities.
For those of you who have joined Codewars since my last invitation, here are a few highlights on what has changed since then:
- We now have a lot more Coq challenges (74 at the time of writing) compared to a year ago (maybe about a dozen or two?) so rest assured you won’t run out of challenges to solve anytime soon
- The difficulty rankings for Coq Kata have stabilized since then. Previously, it was not that uncommon to encounter a beginner-level challenge incorrectly labelled as advanced which made it rather inconvenient for solvers to search for challenges suited to their own level of ability. This has now been fixed and will not happen again for Coq
- We now have a dedicated test framework (coq_codewars) for Coq which allows you to specify what axioms are (dis)allowed on a per-challenge basis. What’s more, the testing framework is powerful enough to support code-golfing challenges and code extraction.
You may learn more about the Coq environment on Codewars through our Wiki page. Feel free to drop by our Gitter chat if you have any questions about Codewars or would just like to chat with fellow Codewarriors.
Happy sparring! 