Un langage sûr

Bonjour,

je suis actuellement en train de lire Types and programming language (pierce etc) et dans l’introduction ils parlent des langages sûr, et c’est un peu brouillon.

Un langage peut être typé, il peut être statiquement vérifié, ou dynamiquement, ou avoir un peu des deux, et pourtant ne pas être safe, selon eux un langage safe c’est un langage qui protège ses propres abstractions, on doit pouvoir déduire le résultat d’un programme avec la doc a coté, et c’est, selon eux, pas le cas des langages comme C et C++, le seul exemple que j’ai en tête c’est qu’on peux aller taper dans des cases de tableaux qui a priori dépassent la capacité qu’on a alloué nous même, et donc se manger un comportement indéterminé.

Mais si dynamiquement ont dégageais des érreurs de bornes de tableau, ça ne ferais pas du C ou du C++ un langage sur pour autant ? j’ai l’impression que chacun a sa petite définition selon ce qu’il utilise mais j’arrive pas a trouver de définition claire et finie de ce que la frontière entre un langage sur et un langage pas sur

Salut,

Il y a des tonnes de façons d’obtenir un comportement indéterminé en C : dépassement de tableaux, accès à de la mémoire non initialisée, suivre un pointeur NULL, situation de compétition…

On pourrait construire un sous-ensemble de C (ou enforcer des règles strictes) qui soit safe (voir ici par exemple, mais ce n’est plus du C.

Merci pour les autres exemples

Je vais en profiter pour poser toute les questions connes que j’ai a poser

Question con 1 : au final on essaye de classer les langages selon la manière dont ils sont typé ou vérifié, mais ça existe pas un langage de programmation non typé ? (je parle des langages vraiment utilisé faut pas me sortir une variante du lambda calcul)

Question con 2 : si un langage sûr c’est un langage sur lequel on est sensé pouvoir déterminer quel seras le comportement du programme avec uniquement la documentation, je veux bien, mais dès qu’on introduit de la concurrence, c’est plus du tout déterministe donc tout les langages, a partir du moment ou ils embarquent de quoi faire manipuler plusieurs threads en meme temps, ne sont plus sûr ? (parce que la on laisse a la charge du dev de taper du code thread safe, pas au langage)

Le but de mon post c’est quand meme, pour le rappeler, de connaitre si elle existe, la frontière claire entre un langage safe et unsafe

Question con 1 : au final on essaye de classer les langages selon la manière dont ils sont typé ou vérifié, mais ça existe pas un langage de programmation non typé ? (je parle des langages vraiment utilisé faut pas me sortir une variante du lambda calcul)

Je comprends pas trop pourquoi il y a un "mais" dans ta phrase. J’ai pas d’exemple qui me vienne de langage non typé, ça n’empêche que des langages avec des typages en mousse qui servent pas à grand chose, il y en a plein (C, bash, PHP, JS par exemple). A contrario, des langages avec un typage fort et bien foutu, il y en a (Haskell, Rust par exemple). Tu as aussi plein d’intermédiaires comme Python (d’un côté si tu essayes de faire quelque chose qui n’a pas d’implémentation, tu te prends une Exception au lieu d’un code qui fait n’importe quoi, les problèmes étant que tout ça se passe au runtime et que la philosophie du duck-typing fait qu’il y a beaucoup de comportements pas forcément souhaitables qui passeront quand même). Donc trier les langages sur leur typage n’est pas déconnant.

si un langage sûr c’est un langage sur lequel on est sensé pouvoir déterminer quel seras le comportement du programme avec uniquement la documentation, je veux bien, mais dès qu’on introduit de la concurrence, c’est plus du tout déterministe donc tout les langages, a partir du moment ou ils embarquent de quoi faire manipuler plusieurs threads en meme temps, ne sont plus sûr ?

D’où tu tiens que la concurrence est non-déterministe ? Voir Rust et Go pour deux langages sûrs (au moins Rust, Go je suis pas sûr) qui repensent la façon de faire de la concurrence et éliminent pas mal de classes de bugs bien chiants à débugger avec les approches classiques genre MPI ou OpenMP.

Le but de mon post c’est quand meme, pour le rappeler, de connaitre si elle existe, la frontière claire entre un langage safe et unsafe

Tu donnes une définition dans ton premier post, qu’est-ce qui te pose problème ?

Question con 1 : au final on essaye de classer les langages selon la manière dont ils sont typé ou vérifié, mais ça existe pas un langage de programmation non typé ? (je parle des langages vraiment utilisé faut pas me sortir une variante du lambda calcul)

Je comprends pas trop pourquoi il y a un "mais" dans ta phrase. J’ai pas d’exemple qui me vienne de langage non typé, ça n’empêche que des langages avec des typages en mousse qui servent pas à grand chose, il y en a plein (C, bash, PHP, JS par exemple). A contrario, des langages avec un typage fort et bien foutu, il y en a (Haskell, Rust par exemple). Tu as aussi plein d’intermédiaires comme Python (d’un côté si tu essayes de faire quelque chose qui n’a pas d’implémentation, tu te prends une Exception au lieu d’un code qui fait n’importe quoi, les problèmes étant que tout ça se passe au runtime et que la philosophie du duck-typing fait qu’il y a beaucoup de comportements pas forcément souhaitables qui passeront quand même). Donc trier les langages sur leur typage n’est pas déconnant.

D’acc

D’où tu tiens que la concurrence est non-déterministe ? Voir Rust et Go pour deux langages sûrs (au moins Rust, Go je suis pas sûr) qui repensent la façon de faire de la concurrence et éliminent pas mal de classes de bugs bien chiants à débugger avec les approches classiques genre MPI ou OpenMP.

D’ou je le tiens ? bah de partout ? tout les cours que j’ai eu/lu en parlent au moins une fois, java c’est sûr, et l’exécution de programmes concurrent bah ça peut etre non deterministe aussi souvent qu’on le souhaite, ou on m’a menti ?

Bah sur le net tout le monde en donne une différente, donc.

Voir Rust et Go pour deux langages sûrs (au moins Rust, Go je suis pas sûr)

Go n’est pas thread-safe en soi (contrairement à Rust), c’est juste qu’il encourage un modèle de concurrence qui contourne le problème de la thread safety : on se passe les données dans des canaux, à chaque instant un seul fil d’exécution manipule la donnée et quand il a fini de bosser avec il la transmet à un autre thread via un canal, donc à moins de faire complètement n’importe quoi on ne risque pas de se marcher dessus. C’est "triché", quelque part, mais c’est diaboliquement simple, et moyennant un petit peu de discipline ça fait des miracles : j’utilise ce modèle de concurrence sur un gros, gros projet en Python au boulot, et sans utiliser de mutexes nulle part (même les canaux en question sont des collection.deque, même pas des threading.Queue !), cela fait des années qu’on n’est pas tombé sur une race condition (alors que la codebase bouge et grossit très vite).

Quant à dire que le multi-thread n’est pas déterministe… oui bon, ok, à un instant T on ne peut pas prévoir dans quel état seront N threads. Mais est-ce que c’est unsafe pour autant ? Dans certains langages (comme Rust), on peut tout à fait prévoir ce qui se passera pour chaque thread pris individuellement.

Alors bien sûr, on ne peut pas être 100% safe, 100% du temps, mais on peut pousser le curseur vers le haut, et les langages vraiment modernes (Rust, Pony, etc.) le font très bien.

Oui, par exemple qu’affiche ce code ? Si ma mémoire est bonne, en fonction des compilateurs, le résultat est différent.

int i = 2;
printf("%d", i++ * ++i);

L’idée véhiculé il me semble c’est que la sémantique, c’est à dire le sens de chaque opération devrait être bien défini. Or, pour la cas précédent, la doc ne fait aucune promesse. Cela a un intérêt : laisser le champ libre au compilateur pour faire des optimisations. Par contre, cela a le gros défaut (à mon avis, et selon B. Pierce) de rendre le comportement de ton programme difficilement prédictible.

Alors oui, le cas que je donne est extrême, et personne écrira ce genre de chose. Mais il existe plein d’autres cas où le comportement du langage est indeterminé.

Enfin, la question "c’est quoi un langage sûr ?" est à mon avis mal posée. Il me semble plus intéressant de parler de garanties offert par le langage de programmation. Les langages ML comme OCaml ou Haskell reposent sur le principe suivant : Well-typed programs cannot go wrong. L’idée véhiculée étant que si le compilateur arrive a inférer puis typer un programme, alors tu as la certitude que ce dernier s’évaluera correctement et renverra une valeur et ne va pas cracher pour une raison quelconque genre segmentation fault.

En pratique, cela permet de rattraper de nombreuses erreurs à la compilation contrairement au C où certaines erreurs (liées à la promotion de type par exemple) sont détectées trop tard, et souvent assez loin du lieu d’origine ce qui rend le débogage compliquée.

Pour avoir de telles garanties sur un langage de programmation, cela demande souvent (même si ce n’est pas le cas de tous les langages comme Rust par exemple) que ce dernier repose sur des fondations théoriques solides et c’est exactement l’objet du livre.

Merci pour vos précisions, je suis impatient de voir ce que le livre va m’apprendre.

Formellement le mot "sûr" ne veut rien dire tout seul, il faut dire : sûr par rapport à quelle spécification. Dans le cas d’un langage, la spécification est une classe d’erreur dont on dit (voire on prouve) qu’elle ne peut pas se produire. Certains exemples typiques de classes d’erreurs sont les suivants:

• Les erreurs mémoire (lectures ou écritures mémoires invalides, en dehors de la mémoire possédée par le programme). Les langages comme Python, Rust ou OCaml sont "sûrs pour la mémoire" (modulo certaines API avancées faites pour faire du bas-niveau), C ou C++ ne le sont pas. La plupart des langages sûrs le sont grâce à une combinaison de raisonnement statique (on ne laisse pas accéder à un champ qui n’existe pas) et de tests dynamiques lors des accès en position arbitraire (pour un tableau).

• Les erreurs d’overflow (dépassement de capacité d’un entier). Les langages comme Racket ou Haskell, qui utilisent les entiers de taille arbitraire par défaut, sont sûrs pour les overflows. La plupart des langages ne le sont pas, pour des raisons de performances.

• Les erreurs de typage : on a une erreur de typage quand on essaie d’effectuer sur une valeur une opération qui n’a pas de sens. Par exemple, essayer de passer un argument à un entier (au lieu d’une fonction), ajouter 3 à une fonction (au lieu d’un nombre), ou essayer d’accéder au premier élément d’une fonction (au lieu d’une paire). Les langages OCaml et Haskell sont sûrs pour les erreurs de typages, Python ne l’est pas.

• Les exceptions non rattrapées : certains langages raisonnent sur les exceptions sur lesquelles un calcul peut échouer; une exception non-prévue pour ce calcul est une erreur. Java a un mode d’exceptions "checkée" qui fait ça et qui n’est pas terribe, sinon il n’y a que des langages expérimentaux / de niche (Koka, Links, Idris…) qui sont sûrs en ce sens, et il sont en général sûrs aussi pour les effets arbitraires (ce n’est pas plus difficile), voir ci-dessous.

• Les effets imprévus : certains langages raisonnement sur les effets de bord qu’un calcul peut effectuer (cette partie du code a-t-elle ou pas le droit de faire l’IO ?). Effectuer un effet non-prévu est une erreur. Haskell est sûr en ce sens.

• La non-terminaison : certains langages peuvent garantir que tout programme termine, ou que certains programmes terminent. Une boucle infinie imprévue est une erreur. Coq, Agda, Idris, Koka sont sûr en ce sens, Haskell et OCaml ne le sont pas.

• les "race conditions": certains langages peuvent garantir que deux fils d’exécution parallèles ne vont pas accéder à la mémoire d’une façon qui brise l’indépendance de leurs exécutions (deux accès parallèles, l’un au moins étant une écriture). Erlang et Rust sont sûrs en ce sens, Java fait un gros effort, C/C++ ne le sont pas.

Une classe d’erreur peut être évitée statiquement (avant d’exécuter le programme), par typage ou analyse statique, ou dynamiquement (en faisant des tests pendant l’exécution). Tester dynamiquement transforme un type d’erreur en un autre : Python est un programme dans lequel il n’y a pas d’accès en dehors des bornes, mais il y a des tonnes de cas d’erreur/exception non rattrapés possible, dont l’exception "accès en dehors des bornes du tableau". Les amateurs de sûreté préfèrent donc les approches statiques — mais elles peuvent augmenter la difficulté d’apprentissage du langage.

Enfin, un langage peut spécifier plus ou moins précisément ce qui se passe en cas d’erreur. Le pire, c’est le C et ses enfants, avec leurs "comportement indéfinis" qui sont la porte ouverte au grand n’importe-quoi (sans façon fiable de savoir si un programme donné a un comportement indéfini ou non). Le mieux c’est une exception qui arrête proprement le programme, ou qui a un mode d’erreur bien spécifié. Certains langages non-sûrs pour une classe d’erreur le sont plus dangereusement que d’autres.

En général, quand on dit informellement qu’un langage est sûr, on sous-entend au moins pour la mémoire et pour le typage (en général). On va parler de "concurrence sûre" si on veut parler de l’absence de races, de "typage des effets" pour les exceptions et effets sûrs (parfois appelé un langage "pur" de façon impropre, puisque la pureté devrait aussi être sûre pour la non-terminaison), et de langage "total" s’il est sûr de tous les points de vue à la fois (en général on pense à mémoire + typage + exceptions + effets + non-terminaison, mais en fait les overflow et les races aussi, même si les langages de niches dans cet espace mettent rarement en avant des entiers machines ou de la concurrence).

Pour le reste @gasche a déjà donné l’essentiel. Juste:

Au fond, ton programme sera exécuté par une machine qui calcule de manière plus ou moins déterministe. La question c’est surtout la part de déterminisme auquel tu peux te fier pour raisonner à propos de ton programme.

Par exemple, te reposer sur des mesures du temps dans la très vaste majorité des cas c’est pas possible. En revanche, se reposer sur la causalité (qui est définie à divers stade, au niveau du langage, mais surtout au niveau de l’architecture d’un processeur) des opérations, c’est acceptable.

A noter par contre que ça ne donne pour autant aucune garantie à propos de son implémentation.

Finalement j’ai exactement les réponses a mes doutes et questions, merci a tout le monde (la définition de la sûreté au sens général ou j’étais à côté de la plaque merci gasche)