Le langage le plus sécurisé que je connaisse c'est Coq [1]. Je cite :
"Coq est un système de manipulation de preuves mathématiques formelles; une preuve réalisée avec Coq est mécaniquement vérifiée par la machine"
" Coq intègre aussi [...] un mécanisme d'extraction [qui] permet d'engendrer automatiquement des programmes certifiés en Objective Caml, Haskell ou Scheme à partir de preuves de leurs spécifications."
Niveau sécurité c'est béton, vôtre programme fait exactement ce qu'il est censé faire, vous l'avez prouvé.
Si vous trouvez cette approche trop violente, vous pouvez regarder du coté de Conqoction [2]. Concoqtion est une extention de MetaOCaml qui est elle même une extension d'Objective Caml. Elle permet d'avoir un système de type très riche appelé types indexées. Par exemple vous pouvez indexer le type des listes par le nombre d'élements dans une liste, ainsi vous pouvez spécifier une fonction sur des listes non vides, des listes qui ont un nombre pair d'élements, ect ...
La vérification des types est fait par inférence autant que possible et par des preuves que vous pouvez faire en Coq.
Il est certes plus complexe de programmer dans ces langages que de pisser du code en priant pour que ca ne merde pas mais la sécurité est bien souvent à ce prix.
# Les langages sécurisés ca existe !
Posté par GTof . En réponse au journal Qu'est-ce qu'un langage sécurisé ?. Évalué à 4.
"Coq est un système de manipulation de preuves mathématiques formelles; une preuve réalisée avec Coq est mécaniquement vérifiée par la machine"
" Coq intègre aussi [...] un mécanisme d'extraction [qui] permet d'engendrer automatiquement des programmes certifiés en Objective Caml, Haskell ou Scheme à partir de preuves de leurs spécifications."
Niveau sécurité c'est béton, vôtre programme fait exactement ce qu'il est censé faire, vous l'avez prouvé.
Si vous trouvez cette approche trop violente, vous pouvez regarder du coté de Conqoction [2]. Concoqtion est une extention de MetaOCaml qui est elle même une extension d'Objective Caml. Elle permet d'avoir un système de type très riche appelé types indexées. Par exemple vous pouvez indexer le type des listes par le nombre d'élements dans une liste, ainsi vous pouvez spécifier une fonction sur des listes non vides, des listes qui ont un nombre pair d'élements, ect ...
La vérification des types est fait par inférence autant que possible et par des preuves que vous pouvez faire en Coq.
Il est certes plus complexe de programmer dans ces langages que de pisser du code en priant pour que ca ne merde pas mais la sécurité est bien souvent à ce prix.
[1] http://coq.inria.fr/coq-fra.html
[2] http://www.metaocaml.org/concoqtion/