Blog personnel d'Arthur Milchior

Je viens de découvrir qu'il existait chez Microsoft un laboratoire Software Reliability Research. Je leur souhaite bonne chance et du courage, je crois que Microsoft a bien besoin d'eux.

Surtout que si vous regardez la page, ils sont quand même 12, après ça, on ne pourra pas dire que Microsoft ne met pas les moyens nécessaire pour s'assurer que leurs programmes fonctionnent bien^[1].

Il se trouve que pour mon stage dans l'équipe Proval à l'Inria, mon travaille depuis début juin consiste à implémenter un algorithme décrit dans un article Efficient E-matching for SMT Solvers écrit par un membre de ce laboratoire.

Pour un papier de 18 pages, où les deux premières et deux dernières donnent le contexte, imprimé en recto-verso, ça veut dire que depuis 3 semaines, je travaille sur 7 feuille A4. Au moins, le papier est très rentable ici! Je prend un jour et demi pour lire un coté d'une feuille! et je ne suis pas encore totalement sur de bien avoir compris la fin.

Certains points m'ont posé problèmes, il y avait quelques fautes dans l'algorithme sur papier^[2], par exemple, une fonction à 5 argument à qui ils donnent 4 argument, une fonction qui n'est pas défini dans un cas qui pourtant se produit.

Le pire étant la faute qui donne un mauvais résultat, mais qui compile bien, et qui ne donne même pas de problème à l'exécution. Ici il s'agit d'un {} à la place de { {} } . Ou en français, si les symboles ensemblistes ne sont pas clair pour vous, ils ont marqué "l'ensemble de substitution, vide", au lieu de marquer "l'ensemble de la substitution vide"... ou plutôt en anglais "the empty set of substitution" à la place de "the set of the empty substitution"...

Oui, c'est pas clair je le sais... pour moi ça ne l'était pas non plus. Dans le doute, j'ai voulu aller voir ce que l'auteur avait fait dans son code à lui. Mais c'était ridicule, chercher du code ouvert sur le site de microsoft, je devais délirer pour avoir tenter de faire ça.

Enfin, fort heureusement, l'auteur à qui j'ai écrit m'a confirmé que les 4 corrections que je lui ai soumis était juste. Et ça, c'est le genre de petit truc qui peut faire bien plaisir à lire. Même qu'il a dit qu'il corrigera le papier sur son site^[3]. Peut-être que ça va vraiment aider, c'est ce qui pousse tant de monde à contribuer au monde du libre, même si c'est bénévolement... Quoi qu'est-ce que j'ai dit? Libre? A flute, je savais que ça clochait quelque part. Parce que par contre, pour la question bénévolement... C'est triste de se dire que j'étais plus payé quand je faisais de la figuration^[4] pour France 2. Je ne vous donnerai pas mon salaire, vos patron serait jaloux de voir des gens travailler pour si peu. Quoi que, en fait, si, je suis payé en crédit par l'école, pour valider la licence et par les connaissance que j'accumule. Enfin je suppose.