Ils ne seraient pas fâchés que, par exemple, on puisse coder ces règles métier dans les types, je pense.
ça dépend de la complexité conceptuelle.
C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant.
Je ne sais pas ou en est la méthode B en est mais j'ai entendu parlé dans mes études (y a plus de 15 ans...), et le seul fait d'arme était le code de la ligne 14, avec les preuves écrites à la main. Si on peut vérifier automatiquement la cohérence des invariants, c'est top.
Le truc pour ne pas avoir l’impression d’écrire plusieurs fois la même chose, c’est que la spec soit déclarative et de plus haut niveau que le code.
Oui, la mode est au modèle. Genre SysML qui sert à générer du code ou autre configuration. Écrire un gros méta-modèle cohérent est par contre, vite très compliqué. Les invariants des modèles UML sont codés avec de l'OCL, qui vérifie les propriétés du modèles, mais rien ne permet de tester la cohérence des règles entre elles.
Après avoir bosser quelques années la-dedans, je pense que le centre n'est pas le modèle, mais les transformations entre modèles. Quand tu as un modèle et que tu génères du code, un rapport, une config, ou que tu gères un diff, tu transformes toujours un modèle en un autre. Le Graal est la transformation bidirectionnelle partielle. Cela semble absurde, mais cela arrive tout le temps. En gros, il s'agit du même modèle sous-jacent, mais présenté sous des formes différentes qui suivent un standard précis (AADL, FACE, AUTOSAR,...), avec des outils différents pour travailler dessus. Des gens ont essayés de "mixer" ces modèles, ils ont eu des problèmes...
Ça te laisse complètement le choix de la manière de trier et ça va t’engueuler si t’as commenté l’appel au tri par erreur.
Je crois que les contrats de Smarteffel fonctionne ainsi. Cela reste de la vérification runtime, mais cela a de la valeur (= cela aide vraiment le codeur). Peut être qu'un code exécuté à la compilation pourrait garantir un certain nombre de propriété, mais les méta-compilateurs m'ont l'air bien compliqué à appréhender.
L’exécution à la compilation est une sorte de "propagation de constante" qui fonctionne aussi avec les containers, cela pourrait peut-faire le job. Existe-t-il un langage qui permet de faire ça ? Les templates de C++ ne sont pas une bonne réponse.
Ou alors que le département vente et le département fabrication utilisent pas la même notion de surface et que donc, les règles sont incohérentes et qu’il faut préciser le modèle.
Je suis récemment tombé sur la méthode DDD (https://en.wikipedia.org/wiki/Domain-driven_design), son idée principale est que se mettre d'accord entre service ne passe pas à l'échelle, et est totalement illusoire. L'idée est de créer un "Bounded context" dont l'intérieur est laissé à l’appréciation de chaque équipe, seul les interfaces doivent être spécifiées en commun. Cela rejoint les préoccupations de découpage du code des micro-services, si tu en as entendu parler.
Mais garde à l’esprit que c’est de la recherche en programmation qu’on parle ici. Il s’agit pas forcément d’avoir des choses utilisables dans la seconde.
Bien sur. Disons que j'ai souvent l'impression que la recherche s'intéresse beaucoup à des domaines qui n'intéressent pas les codeurs. Je me rappelle d'un texte d'un codeurs linux qui lisait des papiers de recherche sur un problème précis d'OS qui était majoritairement monocpu, alors que cela n'existe presque plus, et pour des résultats non reproductibles. Je vois la recherche énorme autour du GADT que peu de personnes comprennent, et de l'autre yacc semble abandonné alors que l'on ne peut pas l'utiliser, si il faut générer de vrai messages d'erreur précis et complet. Ocaml semble avoir compris la valeur d'avoir des messages d'erreurs lisible, mais par contre, il n'a toujours pas de moyen simple d'utiliser du multi-core ou les instructions SIMD.
Je n'ai pas vu non plus de recherche sur un langage pour la génération de code performant, c'est pourtant plus écologique d'avoir un code plus rapide. J'ai vu de la recherche sur la compilation du code C (la lib de transformation de boucle utilisé dans gcc), mais pas sur un langage qui permet au compilateur de mieux faire son boulot (unboxing facile, allocation mémoire minime, gestion des instructions assembleurs spécifiques facilités,...).
La recherche semble aussi focaliser sur la recherche du langage ultime. Mais comment fait-on la migration des centaines de millions de lignes de code existantes ? Comment assurer une transition progressive ? Par exemple comment changer "online" le schéma d'une base de données sans perdre de donnée et pouvoir retourner en arrière si besoin ? Le cas général est terriblement complexe. Comment découper un gros code monolithe pour changer la technologie sous-jacente ? C'est un travail d'ingénieur, mais un outil automatique serait un travail de recherche (plus ou moins comme coccinelle). La manipulation du code vu comme une énorme data structurée ne semble pas à la mode.
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
ça dépend de la complexité conceptuelle.
Je ne sais pas ou en est la méthode B en est mais j'ai entendu parlé dans mes études (y a plus de 15 ans...), et le seul fait d'arme était le code de la ligne 14, avec les preuves écrites à la main. Si on peut vérifier automatiquement la cohérence des invariants, c'est top.
Oui, la mode est au modèle. Genre SysML qui sert à générer du code ou autre configuration. Écrire un gros méta-modèle cohérent est par contre, vite très compliqué. Les invariants des modèles UML sont codés avec de l'OCL, qui vérifie les propriétés du modèles, mais rien ne permet de tester la cohérence des règles entre elles.
Après avoir bosser quelques années la-dedans, je pense que le centre n'est pas le modèle, mais les transformations entre modèles. Quand tu as un modèle et que tu génères du code, un rapport, une config, ou que tu gères un diff, tu transformes toujours un modèle en un autre. Le Graal est la transformation bidirectionnelle partielle. Cela semble absurde, mais cela arrive tout le temps. En gros, il s'agit du même modèle sous-jacent, mais présenté sous des formes différentes qui suivent un standard précis (AADL, FACE, AUTOSAR,...), avec des outils différents pour travailler dessus. Des gens ont essayés de "mixer" ces modèles, ils ont eu des problèmes...
Je crois que les contrats de Smarteffel fonctionne ainsi. Cela reste de la vérification runtime, mais cela a de la valeur (= cela aide vraiment le codeur). Peut être qu'un code exécuté à la compilation pourrait garantir un certain nombre de propriété, mais les méta-compilateurs m'ont l'air bien compliqué à appréhender.
L’exécution à la compilation est une sorte de "propagation de constante" qui fonctionne aussi avec les containers, cela pourrait peut-faire le job. Existe-t-il un langage qui permet de faire ça ? Les templates de C++ ne sont pas une bonne réponse.
Je suis récemment tombé sur la méthode DDD (https://en.wikipedia.org/wiki/Domain-driven_design), son idée principale est que se mettre d'accord entre service ne passe pas à l'échelle, et est totalement illusoire. L'idée est de créer un "Bounded context" dont l'intérieur est laissé à l’appréciation de chaque équipe, seul les interfaces doivent être spécifiées en commun. Cela rejoint les préoccupations de découpage du code des micro-services, si tu en as entendu parler.
Bien sur. Disons que j'ai souvent l'impression que la recherche s'intéresse beaucoup à des domaines qui n'intéressent pas les codeurs. Je me rappelle d'un texte d'un codeurs linux qui lisait des papiers de recherche sur un problème précis d'OS qui était majoritairement monocpu, alors que cela n'existe presque plus, et pour des résultats non reproductibles. Je vois la recherche énorme autour du GADT que peu de personnes comprennent, et de l'autre yacc semble abandonné alors que l'on ne peut pas l'utiliser, si il faut générer de vrai messages d'erreur précis et complet. Ocaml semble avoir compris la valeur d'avoir des messages d'erreurs lisible, mais par contre, il n'a toujours pas de moyen simple d'utiliser du multi-core ou les instructions SIMD.
Je n'ai pas vu non plus de recherche sur un langage pour la génération de code performant, c'est pourtant plus écologique d'avoir un code plus rapide. J'ai vu de la recherche sur la compilation du code C (la lib de transformation de boucle utilisé dans gcc), mais pas sur un langage qui permet au compilateur de mieux faire son boulot (unboxing facile, allocation mémoire minime, gestion des instructions assembleurs spécifiques facilités,...).
La recherche semble aussi focaliser sur la recherche du langage ultime. Mais comment fait-on la migration des centaines de millions de lignes de code existantes ? Comment assurer une transition progressive ? Par exemple comment changer "online" le schéma d'une base de données sans perdre de donnée et pouvoir retourner en arrière si besoin ? Le cas général est terriblement complexe. Comment découper un gros code monolithe pour changer la technologie sous-jacente ? C'est un travail d'ingénieur, mais un outil automatique serait un travail de recherche (plus ou moins comme coccinelle). La manipulation du code vu comme une énorme data structurée ne semble pas à la mode.
"La première sécurité est la liberté"