The Coq mailing list

[Guillaume Claret <guillaume AT claret.me>]

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