Articles
-
2022-03-17
Le projet Coq reçoit le prix Science Ouverte du Logiciel Libre de Recherche
Le 5 février 2022, à l'occasion des Journées européennes de la science ouverte, les prix Science Ouverte du Logiciel Libre de Recherche ont été annoncés. Dans la catégorie Scientifique et Technique, le logiciel récompensé était Coq, dont j'ai représenté l'équipe de développement à cette occasion.
[...] -
2021-11-02
Managing known issues: a refinement of the stale bot approach
There are a few universal problems that maintainers of successful open source projects end up facing. One of them is coping with a large number of open issues. This problem is often unavoidable because the available manpower to fix bugs and limitations rarely scales as fast as the manpower to report them. Therefore, the number of open bugs in the issue tracker of popular projects can end up growing and growing until a point where it becomes hard to manage.
[...] -
2017-12-29
Crowdsourcing, notice parue dans le Dictionnaire des biens communs
Cette année est paru le Dictionnaire des biens communs aux éditions PUF. En accord avec l'éditeur, je reproduis ici la notice Crowdsourcing, dont je suis l'auteur. Le crowdsourcing (ou externalisation ouverte) est une pratique apparue avec le Web, dit 2.0, par laquelle un problème est confié à une communauté d’internautes dont le travail consolidé permet d'y apporter une solution.
[...] -
2017-11-30
Leaving room for proofs of False in an adversarial context
Imagine a crypto-currency-based market for mechanically verifiable proofs of theorems and for programs with proofs that they meet their specifications. Simply described, people can attach bounties to mathematical conjectures and other people can try to come up with a proof. If they manage to do so, they submit a formalized version that will be checked automatically and they will receive the reward. In this market where trust is based on automatic proof checkers, we can imagine how disruptive a proof of False may be.
[...] -
2017-10-31
Notes on successfully migrating 4900 bug reports from Bugzilla to GitHub issues
I started contributing to Coq in 2015. This year, the Coq development team was organizing the first Coding Sprint (later renamed into the Coq Implementors Workshop) and was accepting pull requests on the GitHub repository to get patches from external contributors. Back in these days, almost none of the development was carried out through pull requests (I opened PR #68). Things have changed dramatically since then.
[...] -
2016-12-24
Exploring the Stack Exchange way
Like every programmer, I have known the Stack Overflow Q&A website for a long time now. For our community, it probably was one of the most important innovations of the recent years and it is now a routinely used tool. Have a question on programming? You google it, and you are most likely to find, among the first results, one or several questions on Stack Overflow with good answers to your problem. A little bit like when googling for a general notion, one of the first results should probably be a Wikipedia page.
[...] -
2016-02-23
Does electronic voting undermine democracy?
If you ask a random person in the world of computing, there are good chances they will not have a good opinion on electronic voting. Indeed, this population, more informed than average, knows that there is no information system without flaws, whether they come from bugs, design errors, or intensional insertion of "backdoors". Moreover, the majority of the electronic voting systems in use today require to give the keys of the voting boxes to a "trusted third party", without any possible check on the correct conduct of the ballot, from which a legitimate distrust arises, all the more important when the stakes of an election are great.
[...] -
2016-02-23
Le vote électronique discrédite-t-il la démocratie ?
Si vous interrogez des personnes au hasard dans le monde de l'informatique, il y a de bonnes chances que celles-ci n'aient pas une bonne opinion du vote électronique. En effet, cette population plus informée que la moyenne a conscience qu'il n'existe quasiment aucun système informatique sans failles, que celles-ci proviennent de bugs, d'erreurs de conception, ou d'insertion volontaire de "portes dérobées". Par ailleurs, la plupart des systèmes de vote électronique utilisés aujourd'hui supposent de donner les clés des urnes à un "tiers de confiance", sans contrôle possible sur le bon déroulement du scrutin, d'où une méfiance légitime, d'autant plus importante que l'enjeu de l'élection est grand.
[...] -
2015-12-26
L'internet au service d'une meilleure démocratie ?
Nos systèmes démocratiques sont en crise, si différents soient-ils les uns des autres, certains plus que d'autres nul doute. S'il n'est pas évident de connaître les raisons profondes de cette crise ou de ces crises (ce sera aux historiens du futur de les trouver), les symptômes sont en revanche assez manifestes. Le premier d'entre eux est la perte de confiance dans les élites politiques, qui nous représentent et nous gouvernent. Cette crise de confiance, qui peut trouver sa justification ici dans la déconnexion manifeste des élites avec la réalité, là dans les promesses brisées, là-bas dans la corruption généralisée, a des conséquences politiques bien différentes d'un pays à l'autre.
[...] -
2015-09-21
Pistes pour un roman collaboratif
Aujourd'hui les « solutions collaboratives » sont à la mode ainsi que « l'innovation ouverte » (et plus généralement ce qui est « ouvert »). Peut-on tout créer de manière collaborative ? Quand il s'agit de création artistique on est en droit d'en douter. Cependant on voit fleurir des initiatives s'engageant résolument dans cette direction.
[...] -
2015-05-03
Un premier pas vers la sécurité : vérifiez ma signature
Le mail est un système de communication qui existait déjà aux tout débuts d'Internet et qui est massivement utilisé. Cependant, il est beaucoup moins sûr que les messages privés sur Facebook, le chat de Google, ou encore les applications telles que What's app. Heureusement, on peut prendre des mesures pour en améliorer la sécurité.
[...] -
2015-04-01
Transfert de théorèmes par des isomorphismes
En mathématiques, c'est une pratique très courante que d'identifier deux objets à isomorphisme près. Par exemple, les matrices sont des tableaux de n × m cases (i.e. des fonctions dont l'ensemble de départ est {1, …, n}×{1, …, m} et l'ensemble d'arrivée est un corps K) mais on les identifie à des applications linéaires de l'espace vectoriel Kn vers Km. La principale justification en est que le produit de matrices correspond à la composition d'applications linéaires. Et c'est très pratique en effet, mais comment justifie-t-on la chose rigoureusement ?
[...] -
2015-01-17
La révolution de la science ouverte
Parmi les nombreux domaines qu'Internet a ou est en train de révolutionner, je m'intéresse particulièrement à la collaboration massive, et notamment appliquée à la science. J'ai donc été ravi de découvrir le livre Reinventing discovery de Michael Nielsen. Je recommande vivement la lecture de ce livre à toutes les personnes intéressées mais je vais tâcher de vous en fournir ici un résumé personnel.
[...] -
2014-12-10
A key to massively collaborative math is a good interface for writing proofs
Thanks to all the people who reacted, by various means, to my first blog post on collaborative proofs, I have had a lot of insights on what is most likely to not work in my project. But I am also glad that I found out that all these people were enthusiastic about the overall concept.
[...] -
2014-11-27
La licence GPL est adaptée à un modèle commercial, certes, mais pas n'importe lequel
Dans le monde du logiciel libre, on trouve une foultitude de licences. Choisir la bonne, lorsqu'on commence un nouveau projet n'est pas une tâche évidente. La première recommandation est d'utiliser une licence largement connue et diffusée, car plus solide juridiquement. La licence la plus utilisée historiquement est la GPL. Cependant, cela ne veut pas nécessairement dire que ce soit le bon choix pour tout type de projet.
[...] -
2014-11-06
Getting thousands to millions of people working on a single mathematical proof
There are literally millions of people throughout the world who have a strong mathematical background. A part of them probably enjoyed doing math in class but are not using these skills so much anymore. I bet that if you told these people that they can have an impact on mathematical research through small technical contributions on a website during their leisure time, many would be interested.
[...] -
2014-10-03
Giving each piece of writing an equal opportunity
Many times, a thought crossed your mind that would be worth sharing with others. Sometimes, you started writing something about it and then it remained in your notebook forever. If you feel you have well described your idea / problem / rant / whatever, you may decide to share it with your Facebook friends, or on your blog if you have one. But what about sharing it with "everybody". Maybe it’s worth it but in any case, it is not easy to reach an audience and you’re not necessarily prepared to spend the time it requires.
[...] -
2014-09-15
What good can massive-scale collaboration bring to science?
There are many cases when observable macro-phenomena appear from the combination of many micro-phenomena. This is true of the interaction of elementary particles which compose gas, but this has also been proven to be true of human-related phenomena.
[...] -
2014-08-08
Partage d'idées
Imaginez un site web sur lequel tout un chacun serait en mesure de proposer toutes sortes d’idées dont d’autres personnes pourraient ensuite se saisir afin de les réaliser.
[...]
Abonnez-vous via RSS: