The Coq mailing list

[Kinan Dak Albab <babman AT bu.edu>]

Hello,

This sounds like a very nice idea to me. I think having a centralized directory (such as awesome lists on github) with pointers to individual exercises and their proofs is the best way to go about this.

Also, for individual exercises that either have some interesting twist in terms of reasoning or have some value from a Coq perspective pedagogically, it may be appropriate to write some medium articles about them. This can help inform the software engineering and competitive programming communities about Coq.

codeforces (https://codeforces.com/) and leetcode (https://leetcode.com/problemset/all/) have diverse exercises too, some involving natural numbers, and others involving graphs and trees and other data structures. These are popular websites for people training for programming interviews or programming contests. Coq proofs for such exercises will be a lot fun.

I would be willing to contribute to something like this in my free time

Best,

Kinan

On Mon, Dec 23, 2019 at 2:06 PM Guillaume Claret <guillaume AT claret.me> wrote:

Hello,

Very good idea indeed to help to make Coq known to the developers. To
me, a GitHub repository with either links to some proofs or the proofs
themselves would be good. Maybe one in the style of the Awsome lists
https://github.com/sindresorhus/awesome

Regards,
Guillaume Claret

Le 16/12/2019 à 23:06, Vincent Semeria a écrit :
> Dear Coq clubbers,
>
> In this programming competition
> https://codingcompetitions.withgoogle.com/codejam
> Google challenges the participants to solve computing problems as fast
> as possible, in any programming language. Both the time to program the
> solutions and their execution time count in the competition's ranking.
>
> Usually the problems are stated in terms of natural numbers and the
> execution time limits prevent brute force algorithms. So you often have
> to come up with twisted formulas with many edge cases, and hope that
> your results will match those of Google.
>
> I have seen many videos on the web and posts on Stack Overflow giving
> usual pen-and-paper mathematical proofs of the algorithms, but so far I
> haven't found a Coq database with the corresponding formal proofs. Does
> it exist somewhere, maybe for another programming competition ?
>
> If not, I think it would be nice to do it. First it's fun : it fully
> explains why the black magic formulas do solve the problems. Second, it
> would give some visibility to Coq among the competitors of the code
> jams, who are good developers. A collaborative database would be best,
> where anyone can push a proof when they finish it. Do you know a natural
> place to put this database ?
>
> Regards,
> Vincent