David Mentré's blog

Comme l'année dernière, j'ai fait une présentation à des étudiants ESIR 2 (école d'ingénieur de la Fac de Rennes 1) de l'analyse statique avec l'outil Frama-C et son analyse de valeur. Les sources (format propriétaire, licence Art Libre) et le PDF des transparents sont disponibles, ainsi que les exemples.

When writing a computer program that interact or handle with the physical word, a common need is to manipulate physical units like meter, second or km/h. Most of the time it is up to the programmer to ensure that the physical units are correctly used, even if there are rules to check them (divide only meters by meters, ...). All physicists are routinely checking their equations with those rules. Why not programmers?

So here is a draft of OCaml library to do just that: computations on physical values while ensuring physical units rules are followed (for example, you only add meters to meters, not meters to seconds). Here are the SIunits.mli and SIunits.ml files.

The use of the library are quite simple:

• A set of functions to create values with units from simple floats. For example meter 1.0 (or simply m 1.0) creates a value containing 1 meter;
• A set of utility functions to handle SI prefixes like kilo, to normalize a value (i.e. to remove the scaling factor) or to print it with its units. For example, to enter a length of 160 km one would write kilo (m 160.0);
• A set of four operators, +!, -!, *! and /! to do basic computations on those values. For example, to enter a speed of 160 km/h, one would use let speed = (kilo (m 160.0)) /! (hour 1.0). To compute the distance travelled at previous speed during 120 s, one would do let distance = (normalize_si_value speed) *! (s 120.0) and the program can print 5333.333333 .m;

Internally, I have followed the proposal of "Checking SCADE Models for Correct Usage of Physical Units" paper by using a vector of 8 units: 7 base units (following those defined in the SI system) plus one power of 10 unit for the scaling factor (to handle kilo, mega or more exotic units like hour). In fact, to be really exhaustive one would need some additional units but the current code is really a draft. Then, the rule for addition or subtraction is to check that the units are identical, while for multiplication and division the units of the two numbers are added or subtracted. See the above paper for details.

There is a lot of work to transform this draft code into a real, usable and exhaustive, library:

• Power and root operators;
• Comparison operators;
• Decision operators;
• Dimensionless units;
• Absolute or relative values;
• More prefixes and exotic units;
• And of course of lot of tests for above code.

Right now, I do not intend to extend the current code but if other people are interested, I could work on it and open an OCaml Forge project. If there is a need, let me know.

And now a question for the OCaml experts: would it be possible to replace the dynamic checks currently implemented in this library by static checks using OCaml type system (for example using Phantom types)? I think this is not possible: the base units are like arrays of the same size, you need a more expressive type system to express constraints on them (like Coq's Dependent types). But I would be pleased to be shown wrong. :-)

Comme moi, vous êtes peut-être contraint d'utiliser un système d'exploitation Windows propriétaire au travail. Mais ce n'est pas une raison pour ne pas utiliser des petits^[1] logiciels libres qui facilitent les tâches quotidiennes.

Pour ma part j'utilise :

• Eraser pour l'effacement sécurisé : quand on efface un fichier, son contenu est toujours présent sur le disque, seul l'entrée de ce fichier dans l'index des fichiers a été supprimé (quel que soit le système d'exploitation). Ce petit utilitaire permet de réellement effacer le contenu du fichier ;
• 7zip pour la compression / décompression de fichiers : pour manipuler toutes les archives habituelles, ZIP, GZ, TAR, etc.
• x2go pour l'accès X distant : pour afficher le bureau graphique d'une machine Unix à distance. Il supporte la rupture de connexion réseau, il marche bien avec une connexion réseau de mauvaise qualité, il supporte un répertoire partagé entre la machine distante et la machine locale. Le seul soucis que j'ai eu a été avec le copier / coller, mais le bug a peut-être été corrigé avec les versions récentes ;
• SpeedCruch comme calculette : enfin une calculette qui calcule et qui n'affiche pas simplement un clavier qui ne sert à rien ! On peut désactiver le clavier, régler facilement l'affichage (par exemple en multiple de 1000) ou prendre le point comme séparateur de décimal, même en français (enfin on peut utiliser le point du clavier numérique !), elle a un historique des calculs et offre une coloration syntaxique du calcul en cours. Bref, elle est très pratique. À tel point que j'en avais déjà parlé. :-)
• KeePass pour stocker les mots de passe : cela permet de générer facilement des mots de passe aléatoires et de les stocker dans un fichier chiffré protégé par un unique mot de passe, le seul qu'on soit obligé de retenir.
• NotePad++ comme éditeur de texte : il supporte la coloration syntaxique pour pleins de langages. Par contre, je trouve son interface un peu confuse.

Le seul programme dont je ne suis pas totalement satisfait, c'est DéKiBulle pour écouter les OGG et autres MP3. Si vous avez une meilleur suggestion, je suis preneur !

Je n'ai pas de télévision. Cela peut paraître incongru, mais c'est quand même vrai. Et chaque année, je coche la case « Pas de télé donc pas de redevance » sur ma déclaration de revenus.

Et depuis deux ans, je reçois une lettre amusante :

Objet : Contribution à l'audiovisuel public 2010 - Avis de passage

Madame, Monsieur,

Je me suis présenté à votre domicile le Sem 21/2011 afin de pouvoir vérifier, comme vous l'avez déclaré sur votre déclaration de revenus établie en 2010, qu'aucune de vos résidences n'est équipée d'un appareil récepteur de télévision.

En raison de votre absence lors de ce premier passage, je n'ai pu procédé à cette vérification.

Chose étrange cette lettre est sous enveloppe scellée, reçue par la poste. Et la date est loin d'être précise^[1]. :-) Je ne sais pas vous, mais j'ai du mal à croire que l'inspecteur ce soit déplacé jusqu'à mon appartement, avec une lettre pré-imprimée dans une enveloppe scellée sous le bras, juste au cas où.

La lettre continue (l'italique est de moi) :

Si toutefois vous déteniez un appareil récepteur de télévision, je vous invite à régulariser votre situation .... Un avis d'imposition de 121 euros vous sera ultérieurement adressé et, à titre exceptionnel, aucune amende ne sera appliquée, pour la contribution à l'audiovisuel due en 2010.

En langage clair : on sait que tu as fraudé, mais si tu te dénonces tout de suite on ne dira rien.

Bien sûr, je trouve normal de payer mes impôts, redevance audiovisuelle ou autre. J'écoute abondamment les chaines de Radio France, avec un récepteur radiophonique dans chaque pièce. Donc il serait normal que je paye la redevance audiovisuelle. Je comprends que l'État soit ricrac côté finances et qu'il fasse les fonds de tiroirs. Mais la loi est conditionnée aux récepteurs de télévisions, c'est comme ça. Et je n'aime pas qu'on me prenne pour un imbécile.

Je me suis fait un plaisir de renvoyer le bulletin confirmant que je n'avais pas de télévision. L'année dernière, je n'ai pas vu d'inspecteur.

Camille Landais, Thomas Piketty et Emmanuel Saez on récemment publié « La révolution fiscale, Un impôt sur le revenu pour le XXIe siècle » aux éditions Seuil, 12,50 €. J'en recommande fortement la lecture.

Ce livre est découpé en trois parties. La première partie fait un bilan très pédagogique du système fiscal actuel en partant de données macro-économiques (le Produit Intérieur Brut (PIB), le nombre d'adultes, ...) pour raffiner et expliquer d'où vient l'argent, comment il est prélevé et à qui il est redistribué. On y apprend par exemple qu'en moyenne les français payent 49% d'impôts ou que les 1% de français très aisés (500.000 personnes) détiennent 24% du patrimoine national. Saviez vous par exemple que l'impôt sur le revenu (IRPP) représente seulement 3% du revenu national, contre 6% pour la Contribution Sociale Généralisée (CSG), 13% pour les impôts à la consommation (TVA et autres impôts indirects) et 23% pour les cotisations sociales (maladie, famille, formation, retraite, chômage, ...) ? Autant dire que quand on (nous ou les politiques) se focalise sur l'impôt sur le revenu, on ne regarde qu'une toute petite portion des prélèvements. Plus intéressant encore, les auteurs montrent que notre système fiscal est clairement régressif, les 5% les plus riches payant moins d'impôts que le reste de la population.

La seconde partie décrit la proposition des auteurs : une simplification du système fiscal actuel, pour une meilleure transparence et une meilleure équité. Ils proposent une suppression de l'actuel impôt sur le revenu (IRPP) qui serait remplacée par une CSG aux taux révisés, prélevée à la source, et touchant autant les revenus du travail que du capital. L'impôt serait prélevé par individu, en distinguant notamment les deux conjoints d'un couple pour éviter de pénaliser les femmes qui ont souvent le revenu le plus faible. Ce qui est très intéressant dans cette proposition est que les auteurs ne cherchent pas à augmenter ou diminuer le volume global d'impôt : l'impôt prélevé est le même, seulement plus simple et plus équitable. Et bien entendu, rien n'empêche d'y envisager des modifications, pour être plus « de droite » ou « de gauche » (cf. tableau p. 95). Avec la proposition actuelle, 97% des français payeraient moins d'impôts.

La troisième partie détaille les perspectives possibles : un revenu d'autonomie pour les jeunes adultes, améliorer les transferts sociaux, etc.

Ce livre est accompagné d'un site web, revolution-fiscale.fr, qui contient des simulateurs pour élaborer ses propres variantes de la réforme proposée. Plus intéressant encore, l'intégralité des données et des programmes sont disponibles pour permettre aux plus courageux de refaire et vérifier les calculs^[1]. Il n'y a pas de licence clairement associée à ces données et programmes, mais les auteurs demandent « simplement aux personnes utilisant nos programmes et fichiers d'indiquer leur source », ce qui peut en faire une licence Libre. En tout cas, l'effort de documentation scientifique est significatif et mérite d'être signalé. Même dans le monde scientifique, il est rare de trouver des publications qui fournissent les programmes et données utilisées.

Bien que relativement court, 40 petites pages pour la partie bilan et de même pour la proposition, j'ai trouvé ce livre très pédagogique et très stimulant. N'hésitez pas à l'acheter ou l'emprunter.