L'apprentissage des nouveaux langages

Ouaip, j'y étais. La présentation était bien mais il est resté trop général à mon goût. C'est un peu le problème des confs généralistes de l'UPMC d'ailleurs je trouve.

Faut suivre son cours au MPRI =)

Tout dépend des bugs en question. Il ne faut pas oublier que lorsqu'on analyse des programmes, on se retrouve très rapidement face à des problèmes indécidables, et il faut souvent annoter son code et l'écrire d'une certaine manière pour ensuite pouvoir prouver certaines propriétés dessus. Pas sûr que la majorité des développeurs soit prête à changer ses habitudes de programmation pour quelques garanties supplémentaires (exceptés les domaines critiques comme l'aviation, le spatial etc…).

Ou le voir en conf non généraliste . Je commence à manquer de temps pour suivre des cours.

C'est même certain que non. La majorité des boîtes sont bien plus enclines à vendre des logiciels buggés mais vite et pas cher, pour remporter les marchés et vendre de la maintenance. Après on peut espérer que ce genre de mentalité finisse par changer mais je suis sans doute un idéaliste.

D'où l'idée d'avoir des langages qui nous apportent gratuitement un maximum de garanties fortes par leur simple sémantique. Le principe des nos langages de programmation c'est de nous apporter la bonne dose de restrictions pour garder un maximum de programmes cohérents et de ne pas autoriser le reste.

Et nous fournit les moyens de dire toujours plus précisément ce qu'on attend et plus facilement. Par exemple, pour pouvoir exprimer ce qui nous fait dire que tout est décidable dans notre programme. Où nous permettre d'exprimer des propriétés fonctionnelles qu'on veut assurer, etc.

Pas sûr que la majorité des développeurs soit prête à changer ses habitudes de programmation pour quelques garanties supplémentaires (exceptés les domaines critiques comme l'aviation, le spatial etc…). Source:Bibibye

En fait, si tu regardes les langages typés statiquement fort, je pense notamment aux langages fonctionnels, ces langages imposent une certaine rigueur sur la façon de programmer. Et de nombreux programmeurs sont satisfait avec ces langages. Certes, le typage ne permet pas de prouver actuellement beaucoup de propriétés sur tes programmes, mais ça évolue…

De plus, quand on voit les millions dépensés pour corriger des bogues, ça ne m'étonnerait pas qu'on évolue de plus en plus sur des langages "sûrs".

La question c'est qu'est-ce qu'on est prêt à sacrifier pour avoir un langage sûr, et aujourd'hui le sacrifice est beaucoup trop grand pour qu'on le fasse. Il faudra certainement attendre d'avoir des nouveaux langages avec d'autres mécanismes plus évolués.

Je suis d'accord avec les langages fortement typés : ils permettent d'ajouter des contraintes fortes sur les programmes, et c'est quelque chose que tout le monde est plus ou moins prêt à utiliser. Mais entre ça et corriger la plupart des bugs, il y a un fossé. Et les nouveaux langages auront beau apporter des mécanismes plus évolués, on ne pourra jamais assurer certaines propriétés sur les programmes dans le cas général. Un bug, c'est vaste.

Oui, mais en programmation, on s'aperçoit qu'on est rarement dans le cas général, on n'y est presque jamais en fait. Le problème de la Halt est indécidable dans le cas général. On s'en tape, sur la majorité des programmes qui nous intéressent, on y arrive. On s'intéresse au cas spécifiques des applications qui font ce qu'on leur demande. En l'occurrence, en preuve on ne s'intéresse pas tant à assurer que le programme ne fait pas de choses que l'on ne veut pas mais plutôt à s'assurer qu'il ne fait que ce que l'on veut.

Et les contraintes de typage peuvent encore aller bien plus loin qu'elles ne vont actuellement. Intégrer le PpC dans le typage d'un point de vue théorique, c'est loin d'être impossible.

Un compilateur / interpréteur doit pouvoir fonctionner dans le cas général. C'est pour ça qu'il faut ajouter des annotations pour spécifier les cas particuliers dont tu parles, et permettre au compilateur de faire des vérifications avec ces annotations.

Bien sûr qu'on arrive à prouver des choses sur des programmes particuliers, mais pas automatiquement. Je ne dis pas qu'on ne peux rien faire, simplement qu'il ne faut pas s'attendre à des outils magiques, et que chaque vérification supplémentaire sur un programme vient avec une contrepartie (ajouter des annotations en est une). La question va donc être de trouver le point idéal : assez de vérifications sans trop s'embêter.

Je suis tombé par hasard sur un langage, Pony, qui m'a l'air assez intéressant pour les questions de sureté.

Je vous laisse juger par vous même :

• It's type safe. Really type safe. There's a mathematical proof and everything.
• It's memory safe. Ok, this comes with type safe, but it's still interesting. There are no dangling pointers, no buffer overruns, heck, the language doesn't even have the concept of null!
• It's exception safe. There are no runtime exceptions. All exceptions have defined semantics, and they are always handled.
• It's data-race free. Pony doesn't have locks or atomic operations or anything like that. Instead, the type system ensures at compile time that your concurrent program can never have data races. So you can write highly concurrent code and never get it wrong.
• It's deadlock free. This one is easy, because Pony has no locks at all! So they definitely don't deadlock, because they don't exist.

Bon, c'est un peu du déterrage, mais cette phrase tourne dans ma tête … Pourquoi pas Rust ? Je trouve justement que ce langage remplace super bien le C++ en étant supérieur d'un point de vue théorique (sémantique, safety, cohérence) que pratique (gestionnaire de dépendances, auto-formatage du code, workflow). Il manque en effet la programmation par contrat incluse dans le langage, mais elle est au même niveau que C++ (assert de partout); et les outils de preuve, mais je n'en vois pas vraiment l'intérêt.

De ce que j'ai lu ici et là, la performance des exécutables générés (bien que très bonne actuellement) n'est pas l'objectif principal du développeur principal (Mozilla), au profit plutôt de sa sûreté. Alors, c'est un choix qui se comprend tout à fait, j'ai pas fondamentalement de problème avec ça, mais le fait est que s'ils veulent concurrencer C++ sur son terrain de jeu, ça risque de poser problème. Il y a pas mal de domaine ou tu ne peux pas te permettre de perdre 3% de performances même pour gagner 30% en safety.

Pour préciser ce que j'entends pas "Non, pas Rust" : ce n'est pas que je ne pense pas que Rust aille dans le bon sens sur le plan safety et clarté, je suis même persuadé qu'ils vont dans le bon sens, c'est que je pense que s'ils ne font pas de la performance leur objectif prioritaire, il ne remplacera pas facilement C++.

Et quand je parle de faire de la performance une priorité, je ne parle pas d'intégrer des possibilités plus unsafe et des faiblesses sémantiques. Je parle d'accepter que tout ne soit pas parfait côté processus de compilation et de faire des optimisations très agressives, limite unsound.

Il me semble que l'idée n'est pas de concurrencer mais de proposer une alternative. Donc en soit, le boulot est là. Un peu moins performant mais plus safe. Je pense que Rust trouvera sa place.

Et quand je parle de faire de la performance une priorité, je ne parle pas d'intégrer des possibilités plus unsafe et des faiblesses sémantiques. Je parle d'accepter que tout ne soit pas parfait côté processus de compilation et de faire des optimisations très agressives, limite unsound.

Ok, je vois mieux ton point de vue. En effet, les dev de chez Mozilla ne voudrons sans doutes pas activer d'optimisations unsound, mais la performance reste un objectif prioritaire au vu de leur page d'acceuil:

(l'emphase est mienne)

Je vais me faire lyncher mais Swift a des performances avoisinant celles de C++, tout en étant de très haut niveau. Il est type safe et gère plein de trucs sympa comme les attributs évalués paresseusement, le pattern matching, les guards, les extensions, les properties et le système d'énumérations est génial.

Le seul inconvénient c'est que pour l'instant ça ne fonctionne pas sous Windows.

Edit: d'ailleurs j'aimerais bien avoir des retours de votre part sur Swift parce que pour l'instant je n'y vois pas d'inconvénient… Celui qui m'a poucerougé pourrait-il expliquer pourquoi il n'aime pas Swift ?

La lecture de ce thread a fini par me convaincre de me frotter à Rust. Il semble matcher assez bien au complément moderne de Python que je cherche depuis des lustres (i.e. langage système, compilé, bind-able en Python, performant et proposant des mécanismes d'abstraction youpilol). Par contre il faut être conscient que c'est pas le genre de compétence facile à vendre… du moins pas directement ni à court terme.

Perso je trouve Rust très intéressant théoriquement, en pratique ça utilise des concepts beaucoup trop compliqué pour le commun des dev qui n'arrivera jamais a véritablement percé. Il pourra connaitre une certaine utilisation dans des cas précis mais ça restera un langage de niche.

Kje, quels sont ces concepts ?

Il parle probablement de la propriété, des durées de vie et des emprunts.

Rien que la "move semantics". C'est introduit aussi en C++11 et pourtant je vois assez peu de code les utiliser, encore moins correctement.

Je ne dis pas que c'est insurmontable, simplement que ce sont des concepts plus "complexe" que dans de nombreux langage. De nombreux dev ne passeront jamais le cap.

Après Rust n'a jamais eu pour vocation de devenir LE langage pour convenir à tout le monde. Le site dit clairement que c'est un langage orienté système. Donc il est peu probable qu'il devienne mainstream, il restera probablement toujours dans sa niche.

Après, je suis pas persuadé qu’il soit nécessaire de véritablement comprendre le concept de la sémantique de mouvement pour la mettre en pratique telle qu’elle existe en Rust. De ma (courte, je le reconnais) expérience personnelle, j’ai quand même l’impression qu’à partir du moment où tu te dis « tout le monde peut lire le registre, mais une seule personne à la fois peut l’avoir sur son bureau et écrire dedans, comme ça il n’est jamais perdu », tu as compris à peu près tout ce qu’il faut comprendre pour faire un code qui compile.