SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne > comporte pas d’ambigüité. Et le compilo est certifié.
Tout ce que tu dis est vrai (et pour cause !), je préciserais simplement que "ne pas comporter d'ambigüité" veut dire qu'on peut donner au langage une sémantique formelle claire. Ça va aussi avec un certain nombre d'articles de recherche présentant le langage et diverses techniques de compilation de façon très propre. Un compilateur prouvé correct en Coq pour une version très antérieure de SCADE, Lustre, a d'ailleurs été récemment présenté à la conférence PLDI.
Why3 est ce qu'on appelle un générateur de conditions de vérification, c'est à dire un outil transformant un programme contenant des spécifications formelles (typiquement formulées sous la forme de pré- et post-conditions) en un ensemble de formules logiques (les dites conditions de vérification) dont la validité implique que le programme respecte sa spécification. Une fois générées, Why3 transmet ces conditions de vérification à divers outils pour essayer de démontrer leur validité automatiquement; celles pour lesquelles ce processus échoue sont traduites vers Coq pour permettre la preuve manuelle.
(Par ailleurs, l'auteur principal de Why3 est aussi un des contributeurs historiques au cœur de Coq.)
[…] est-ce que les chercheurs en programmation (financés par l'argent public, etc.) devraient avoir comme finalité dans la vie d'aider l'industrie à écrire du code crade et jetable plus vite qu'avant ? […] Et rendre les programmeurs jetables/interchangeables en uniformisant les outils et techniques (une autre chose dont les managers dans l'industrie auraient bien envie), on devrait travailler dessus aussi ?
Je pense que c'est plus ou moins explicitement l'objectif d'une large partie de la recherche en ingénierie logicielle qui a lieu en France et à l'étranger.
C'est chouette de partager ton code avec d'autre dans l'espoir qu'il soit utile. Merci !
Petite question : pourquoi avoir choisi C++ pour un programme qui consiste essentiellement à manipuler des chaînes de caractères puis à les passer au shell ? Il me semble que ce n'est pas connu pour être une des grandes forces du langage.
Posté par auve .
En réponse au journal Word vs TeX.
Évalué à 3.
Ça serait bien que la solution WYSIWYM du XXIe siècle vienne du libre, parce que si ça n'est pas le cas, on ne pourra pas résister très longtemps, ne serait-ce que pour une simple raison de productivité.
On m'a dit du bien de Patoline. Ils refont à la fois le langage d'entrée, histoire d'avoir quelque-chose de plus raisonnable et moderne que TeX et LaTeX, et le moteur de rendu lui-même. Je ne sais pas trop ce que ca vaut, ne l'ayant pas utilisé moi-même.
Uniquement de son vivant, vu qu'il voulait que tout soit détruit à sa mort.
Je ne crois pas que cela ait été son intention, à en croire la lettre trouvable sur http://www.grothendieckcircle.org et reproduite dans le billet de David Madore cité plus haut :
Toute édition ou diffusion de tels textes qui aurait été faits par le passé sans mon accord, ou qui serait faite à l'avenir et de mon vivant, à l'encontre de ma volonté expresse précisée ici, est illicite à mes yeux.
Oui mais voilà, dans la pratique, cela donne des clés gigantesques (plusieurs méga-octets, alors qu'une clé RSA ne pèse qu'entre 128 et 512 octets), et les calculs (addition et multiplications) peuvent être jusqu'à 1000x plus lents que les opérations non-homomorphes.
Parce que le hardware est comme ça, et que spécifier la sémantique d'un programme contenant des data-races de façon portable et sans inhiber les optimisations faisables par le compilateur est quasiment impossible à l'heure actuelle ?
Et ce certificat de certification a été automatiquement accepté comme légitime par ton navigateur (i.e. les certificats "finaux" signés par celui-ci sont acceptés), simplement parce qu'il existe un chemin de confiance entre lui et un certificat racine, où cela a réclamé une procédure supplémentaire ?
Et si elle signe un certificat de certification pour un gouvernement ?
Hum, je crois que le fonctionnement de l'infrastructure à clé publique t'échappe complètement. Les certificats racines ne peuvent pas servir à en créer de nouveaux qui seraient automatiquement acceptés par ton navigateur. Encore heureux !
Posté par auve .
En réponse au journal gnome3.org.
Évalué à 3.
Sorti des applis du dock, j'ai juste compris qu'on devais se farcir le finder et le répertoire Applications, ou tout est en vrac. Tout sauf utilisable.
Euh un macounet ayant besoin de plus de cinq applications fera ctrl - espace pour afficher Spotlight (le service de recherche d'OSX), tapera une partie du nom de l'appli qu'il veut lancer, et appuiera sur entrée...
Dans les 15'6 (je ne sais pas si tu les comptes comme des 15 pouces), y a quand même un paquet de portables avec écrans dits "1080p"... Regarde chez Sony (Vaio) ou Dell (XPS L510x et assimilés). Les Vaio doivent probablement t'offrir de bonnes résolutions en 13'.
Sinon, le MacBook Air 13' a une résolution de 1440x900.
Je l'ai fais de tête c'est un oublie simple à prendre en compte.
Euh, si tu ajoutes une version correcte de la fonctionnalité demandée par Bruno (dépendance vers les headers utilisés par un .c) à un Makefile aussi simple, ça devient de loin la partie la plus compliquée...
N'empêche, si deux mecs motivés arrivent à faire ça, je me pose la question de 10 mecs payés pour faire de l'espionnage industriel par exemple...
Euh certes, mais ta phrase peut laisser penser que les gens en question étaient de gentils gus dans leur garage qui ont fait ça un dimanche après-midi, alors qu'en pratique ils sont/étaient chercheurs en sécurité informatique chez EADS et en ont largement chié d'après mes souvenirs. À mon avis ils rentrent pour une large mesure dans la case « payés à faire de l'espionnage industriel » !
[^] # Re: Le cerveau n'est pas logique
Posté par auve . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Tout ce que tu dis est vrai (et pour cause !), je préciserais simplement que "ne pas comporter d'ambigüité" veut dire qu'on peut donner au langage une sémantique formelle claire. Ça va aussi avec un certain nombre d'articles de recherche présentant le langage et diverses techniques de compilation de façon très propre. Un compilateur prouvé correct en Coq pour une version très antérieure de SCADE, Lustre, a d'ailleurs été récemment présenté à la conférence PLDI.
[^] # Re: Le cerveau n'est pas logique
Posté par auve . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 6.
Why3 est ce qu'on appelle un générateur de conditions de vérification, c'est à dire un outil transformant un programme contenant des spécifications formelles (typiquement formulées sous la forme de pré- et post-conditions) en un ensemble de formules logiques (les dites conditions de vérification) dont la validité implique que le programme respecte sa spécification. Une fois générées, Why3 transmet ces conditions de vérification à divers outils pour essayer de démontrer leur validité automatiquement; celles pour lesquelles ce processus échoue sont traduites vers Coq pour permettre la preuve manuelle.
(Par ailleurs, l'auteur principal de Why3 est aussi un des contributeurs historiques au cœur de Coq.)
[^] # Re: go 2.0
Posté par auve . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 2.
Je pense que c'est plus ou moins explicitement l'objectif d'une large partie de la recherche en ingénierie logicielle qui a lieu en France et à l'étranger.
# Choix du langage
Posté par auve . En réponse au journal Simple Provisioning System. Évalué à 5.
Salut,
C'est chouette de partager ton code avec d'autre dans l'espoir qu'il soit utile. Merci !
Petite question : pourquoi avoir choisi C++ pour un programme qui consiste essentiellement à manipuler des chaînes de caractères puis à les passer au shell ? Il me semble que ce n'est pas connu pour être une des grandes forces du langage.
# Bingo
Posté par auve . En réponse au journal [ANN] Channel IRC Sur le Domain Driven Design #dddfr. Évalué à 10.
FOUTAISES !
[^] # Re: Et si on prenait ça comme un retour?
Posté par auve . En réponse au journal Word vs TeX. Évalué à 3.
On m'a dit du bien de Patoline. Ils refont à la fois le langage d'entrée, histoire d'avoir quelque-chose de plus raisonnable et moderne que TeX et LaTeX, et le moteur de rendu lui-même. Je ne sais pas trop ce que ca vaut, ne l'ayant pas utilisé moi-même.
[^] # Re: La géométrie algébrique et le reste...
Posté par auve . En réponse au journal Alexandre Grothendieck est bronsonisé. Évalué à 4.
Je ne crois pas que cela ait été son intention, à en croire la lettre trouvable sur http://www.grothendieckcircle.org et reproduite dans le billet de David Madore cité plus haut :
[^] # Re: Plutôt beauté du design
Posté par auve . En réponse au journal "beauté du code". Évalué à 5.
Tout le monde aimerait que ce soit vrai mais c'est une légende urbaine. John Carmack n'a pas écrit cette fonction.
[^] # Re: TV
Posté par auve . En réponse au journal Un billet de réflexion sur l'échec de Linux sur le Desktop. Évalué à 10.
Venant du concepteur historique de C++, c'est vraiment la paille de l'hôpital qui se fout de la poutre de la charité…
[^] # Re: En pratique
Posté par auve . En réponse à la dépêche Le chiffrement homomorphe. Évalué à 2.
Je cite l'article :
[^] # Re: Modestie...
Posté par auve . En réponse à la dépêche Un entretien avec Lennart Poettering. Évalué à 3.
Steve Jobs t'a fait quelque-chose quand tu étais petit ? Sûrement la même chose que Bill Gates à Albert_.
# Je vais donc aussi...
Posté par auve . En réponse au journal Fermez les écoutilles. Évalué à 10.
... arrêter de lire les journaux de DLFP.
[^] # Re: Un dernier petit pas pour C++0x
Posté par auve . En réponse à la dépêche La version 4.6 du compilateur GCC est disponible. Évalué à 1.
Parce que le hardware est comme ça, et que spécifier la sémantique d'un programme contenant des data-races de façon portable et sans inhiber les optimisations faisables par le compilateur est quasiment impossible à l'heure actuelle ?
http://rsim.cs.illinois.edu/Pubs/10-cacm-memory-models.pdf
[^] # Re: Pas besoin de MS
Posté par auve . En réponse au journal Où l'on parle de Microsoft et des méthodes démocratiques de Ben Ali.... Évalué à 1.
Et ce certificat de certification a été automatiquement accepté comme légitime par ton navigateur (i.e. les certificats "finaux" signés par celui-ci sont acceptés), simplement parce qu'il existe un chemin de confiance entre lui et un certificat racine, où cela a réclamé une procédure supplémentaire ?
[^] # Re: Pas besoin de MS
Posté par auve . En réponse au journal Où l'on parle de Microsoft et des méthodes démocratiques de Ben Ali.... Évalué à -2.
Hum, je crois que le fonctionnement de l'infrastructure à clé publique t'échappe complètement. Les certificats racines ne peuvent pas servir à en créer de nouveaux qui seraient automatiquement acceptés par ton navigateur. Encore heureux !
# On peut rire de tout...
Posté par auve . En réponse au journal [Breaking News] Impacts du tremblement de terre sur DLFP. Évalué à -10.
... ou pas.
[^] # Re: Glissement de la source ?
Posté par auve . En réponse au journal Symbian, Moblin/Meego et Android sont dans bateau nommé Nokia. Évalué à 4.
[^] # Re: Critique sans avoir essayé
Posté par auve . En réponse au journal gnome3.org. Évalué à 3.
Euh un macounet ayant besoin de plus de cinq applications fera ctrl - espace pour afficher Spotlight (le service de recherche d'OSX), tapera une partie du nom de l'appli qu'il veut lancer, et appuiera sur entrée...
[^] # Re: Oui mais non
Posté par auve . En réponse au journal Un portable 15.6" sous GNU/Linux à prix plancher !. Évalué à 0.
Sinon, le MacBook Air 13' a une résolution de 1440x900.
[^] # Re: Il faut résonner en terme de Toolkit et non en tant que DE
Posté par auve . En réponse au journal Qt dans Ubuntu. Évalué à 7.
[^] # Re: J'attends désespérément un moteur de production potable...
Posté par auve . En réponse à la dépêche Redo, un remplaçant de choix pour Make. Évalué à 1.
[^] # Re: make ?
Posté par auve . En réponse à la dépêche Redo, un remplaçant de choix pour Make. Évalué à 3.
Euh, si tu ajoutes une version correcte de la fonctionnalité demandée par Bruno (dépendance vers les headers utilisés par un .c) à un Makefile aussi simple, ça devient de loin la partie la plus compliquée...
[^] # Re: L'hypocrisie d'Apple
Posté par auve . En réponse au journal [BreakingNews] VLC retiré de l'iOS AppStore !. Évalué à 4.
[^] # Re: Jabber HS hier soir
Posté par auve . En réponse au journal Skype HS hier soir. Évalué à 2.
Euh certes, mais ta phrase peut laisser penser que les gens en question étaient de gentils gus dans leur garage qui ont fait ça un dimanche après-midi, alors qu'en pratique ils sont/étaient chercheurs en sécurité informatique chez EADS et en ont largement chié d'après mes souvenirs. À mon avis ils rentrent pour une large mesure dans la case « payés à faire de l'espionnage industriel » !
[^] # Re: Non, mais perso ....
Posté par auve . En réponse au journal C++ a été créé pour augmenter le salaire des programmeurs. Évalué à 1.