Dans les faits, la cohérence interne que tu peux vérifier est assez faible. Comme les gens détestent écrire les choses 2 fois, tu te retrouves à faire des calculs avec des données que tu as déjà, plutôt que vérifier que 2 valeurs sont cohérentes.
Pour l'exemple que tu donnes, cela tombe exactement dans ingénierie des modèles et le genre de petites règles que tu peux écrire. C'est très utile, tu peux augmenter très largement la productivité des utilisateurs. Mais tu ne vérifies pas de cohérence en soi, tu écris la règle elle-même. On est très loin d'une "vérification formelle".
La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet.
Pour ça, il faut un "modèle du monde", ce qui n'existe jamais. C'est le boulot de dingue qui consiste à modéliser toutes les instructions assembleur dans compcert. Donc, non, tu n'as rien de facile sous la main pour confronter ce qu'écrit une personne du métier. Ce qui est typiquement fait, c'est d'utiliser des simulateurs maisons ou pas. Une équipe du métier conçoit un nouveau logiciel de pilote automatique, il va simuler des scénarios pour le valider. Il n'y a pas de règles statiques pour valider qu'il fait n'importe quoi dans certain cas. Dans le cas de ingénierie des modèles, on peut toujours écrire des règles qui permettent de vérifier certaine propriété, c'est forcément limité.
L'autre info c'est de voir le renforcement de alphagoZero en jouant contre lui-même en simulant des parties. Il devrait en théorie être possible de faire une IA qui apprend en utilisant un simulateur. C'est très théorique, je suis d'accord, mais cela serait la porte d'entré de l'IA dans l'ingénierie.
Le "modèle métier" se confronte toujours à une simulation. D'ailleurs, j'imagine qu'un jour les IA s'amuseront directement avec ce genre de simulateur.
Par exemple, le GC de go 1.9 fait maintenant des pauses maximum de 9 ms et utilise des threads. Mais il prends un peu plus de temps cpu pour vérifier la totalité de la RAM. Cela veut dire que pour un serveur chargé qui marche bien actuellement, le nombre de transaction par seconde risque de baisser, même si la latence moyenne pour chaque requête baisse.
Dans l'outil d'ET, il y a un prouveur qui marche assez bien (surtou avec les machines d'état). Je lui est déjà fait trouver des contres-exemples, mais personne ne l'achète ni ne s'en sert.
(si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Le bug peut être également dans le model. J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
J'ai entre autre appris, que les spécialistes métiers ne sont pas des informaticiens et encore moins des matheux. Et que pour décrire leur système, ils ne veulent surtout pas avoir à faire à ce genre de concept. Ils veulent pouvoir décrire des problème spécifique, les exemples de why3 dont parlait mon commentaire, n'ont aucun rapport avec des problèmes industriels.
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier. C'est le sujet du journal.
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
Dans un vieux journal, je parlais d'un langage que j'ai tenté décrire suivant la mode des langages systèmes, un truc qui ressemble a du xml mais avec une notion de nommage pour faire des graphs acycliques. Le truc est mal définit mais bon. Je me demandais si il n'était pas plus sage d'utiliser un truc costaux comme coq ou pourquoi pas why3 pour vérifier le fichier au lieu de le faire à la main. L'idée est d'avoir un langage structurel très user-friendly, dont la vérification est sous traité. L'idée est qu'un langage structurel est plus facile à vérifier.
compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne". De plus la preuve formelle n'est pas encore reconnu dans les certifications aéronautique, en tout cas dans la do178b, je crois que cela bouge un peu dans la DO178C. Et encore, j'imagine que le prouveur lui-même devrait être certifié… Donc, on est pas prêt de voir un avion volé avec un tel code sans certification "papier" à coté. L'outil de ma boite utilisait l'outil de prover, mais c'était peu/aps utilisé car la norme n'en voulait pas.
Pour le reste des échanges, j'arrête là : je pisse dans un violon, tu ne connais pas grand chose aux sujets abordés mais tu parles quand même, ça me saoule.
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
Après, l'arrêt d'urgence fonctionne dans tous les cas reste assez vague comme contrat. On peut juste dire qu'il ne fera pas d'exception à l'exécution.
Tu crois que cela ressemble à quoi des vrai spec ? :) Je faisais un référence un peu trop subtile à un défaut d'un cruise control de toyota qui s'est fait démonté par un expert aéronautique pour un procès : il ne se désactivait pas si la pédale de frein était enfoncé…
En gros, cela voudrait dire que quelques soit les autres entrés, l'arrivé de l’arrêt d'urgence doit arrêter les moteurs.
Il ne faut pas se voiler la face quand même, il est peut être compliqué d'écrire les contrats de façon à ce qu'ils puissent être prouvés
Je sais bien, c'est d'autant plus difficile que le langage de la preuve est éloigné du langage métier, ou du langage de dev.
Concernant le code du drone, on dirait qu'il a seulement fait attention au overflow de calcul. Il faut que je relise moins en diagonal, je n'ai pas vu de propriété spécifiquement vérifier (genre l’arrêt d'urgence fonctionne dans tous les cas).
Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).
Plein de choses :
- ton exemple n'a rien à voir avec un truc réel. Je parlais de typage statique, le genre de truc que l'on trouve dans ocaml, qui ne permet pas ce que tu écris.
- ton exemple n'a jamais été passé dans un prouveur automatique, la démo est manuelle (frama-c ?)
- il faut que l'expressivité soit compréhensible par le commun des mortels, why3 a l'air sympa comme coq, mais il faut être un matheux pour s'en servir. frama-c est un sous ensemble du C, et n'est même pas optimisant !
- c'est très rare d'avoir une spécification aussi simple, un compilo qui optimise, on compare le comportement de sa génération de code sans optimisation, et on colle un fuzzer devant. Imagines le bordel de convertir 500 HLR dans ce genre de langage.
- pour avoir bosser avec un prouveur, l'idéal est de pouvoir écrire un truc dans le même langage et lui demander si la sortie est toujours vrai. Dans le cas contraire, il fournit un contre-exemple. C'est juste énorme. En général, il répond qu'il ne sait pas faire.
Le typage statique est un tel outil. La plupart des systèmes de types n'évitent pas la nécessité de recourir à des tests unitaires, mais ils permettent de capturer certaines erreurs de raisonnement.
Le problème est que tu n'attrapes pas grand chose comme erreur avec un système de typage. La seul architecture que j'ai trouvé pour aider est de transformer un arbre en un autre, sans aucune information redondante ni inutile. Ainsi, un mauvais usage ne compile pas, et on ne traine pas l'entrée à l'intérieur du code. Cela marche bien dans les "filtres unix" mais dans rien d'autre, pour des raisons de performances si les données sont énormes ou pour des raisons pratiques comme l'optimisation d'un AST qui doit donner aussi un AST.
Si on regarde le gadt, la complexité est encore plus grande sans réellement attraper une énorme quantité de bugs supplémentaires. En gros, la complexité devient exponentielle, pour attraper des bugs de façon linéaire.
J'ai discuté avec l'auteur français de smarteffel(?), qui utilise beaucoup les contrats, il disait qu'en codant, il violait régulièrement même des contrats de base présent dans les containers, car la pile d’héritage en bénéficiait (les contrats n’héritent). C'était d'une grande aide pour lui.
Le problème est que le contrat est runtime et nécessite un test pour s’exercer. Il n'est pas possible d'avoir des contrats compile-time ou de vérifier leur cohérence entre eux ?
il est vrai que le langage des modules et foncteurs est assez verbeux.
Attention, la concision est souvent l'ennemi de la clarté. VHDL et ADA sont très verbeux mais très lisible. Je pense que l'abus de symbole est horrible pour la lecture. L'exemple typique sont les regexp Perl qui sont un cauchemar à lire, mais pas à écrire.
Je me demande même si les symboles ne prennent pas "plus de place" dans la tête car il ne se prononce pas, sauf les symboles de base (+).
module type M = sig
type t
val v : t
end
Pour moi, ce truc est bizarre car 2 mots clef se suivent ce qui est très rare ("Module type"), ensuite je lit "M = sig", sig étant un mot clef et ne m'indique pas du tout le début d'une liste qui se fait d'habitude avec des '(' ou des '{' ou des '[' voir des '<'. Ensuite, il y a le ':' qui alourdit la notation, alors que ocaml est ultra light d'habitude (pas de ',', ni de '(').
En go, cela donnerait :
type M module {
type t
var v t
}
(les types sont des valeurs comme les autres et vivent dans le même monde),
C'est génial ça, il existe un autre langage où c'est possible, ou c'est impossible à compiler ?
module type Showable = sig …
Tu te rends compte qu'en go, cette fonctionnalité se fait simplement avec une fonction String() dans un objet ? Elle est reconnu comme présent dans la bonne interface, et le tour est joué.
type Stringer interface {
String() string
} // est définit dans le code du package fmt
Les deux syntaxes sont assez proches : ce sont les mots-clés qui changent. Cela me semble utile, voire conseiller au niveau du principe de moindre surprise,
Non, elles ne sont pas proche justement, ni symétrique.
il serait surprenant que la syntaxe ne le signifie pas par un moyen quelconque : autrement on risquerait de confondre les deux notions.
C'est le but. Coq lui même ne fait pas la différence entre type et valeur, et c'est plus simple.
Je trouve la généricité, les modules très utile. Mais je trouve que leur forme dans ocaml est très complexe et très peu lisible. Cela parait peut être évident pour toi qui est tombé dedans que tu es petit. Mais pour un concept complexe, il faut qu'il ressemble le plus possible à quelques choses de connu (principe UX de moindre surprise). Les modules ressemblent ici vaguement à des objets, avec des définitions de type dedans, mais avec une autre syntaxe.
En fait, je pense qu'il doit être possible de proposer des modules en GO mais avec une syntaxe ultra simplifié pour la compréhension.
Genre :
package toto (type t, int i)
func sort(tab t[i]) {…
import "toto"(int, 1024) -> l'idéal serait d'avoir un seul module instancié pour ce couple de paramètre
Pour l’extension d'un package, j'imagine qu'il doit y avoir déjà l'équivalent d'un "open".
En fait, je pensais au cas d'usage qui reviennent au même. Dans l'esprit, c'est 3 façon d'écrire la même chose, c'est anti-ergonomique, même si c'est formel.
let rp : pt_2D = {x = 1.0; y = 2.0}
let op : obj_pt_2d = object method x = 1.0 method y = 2.0 end
module MP : mod_pt_2D = struct let x = 1.0 let y = 2.0 end
Ils veulent des exemples, et nous on voudrait les types sum. Ils manquent sans doute une bonne explication entre les 2.
L'idéal serait de faire la même chose pour transformer les packages en module, en rajoutant une déclaration "parameter" pour définir des paramètres à remplir à l'import d'un package ou simplement d'ajouter une liste de paramètre à la déclaration de package, puis de fixer un moyen de créer des package "complet" avec ses paramètres. Cela évite un peu la duplication de code, si l'instanciation est faite une seul fois. Si la syntaxe de ces paramètres est exactement symétrique avec des paramètres de fonction, cela devrait rester simple. Il reste la création de signature de package dont je ne vois pas trop à quoi il pourrait ressembler en go. L'idéal serait qu'un package soit à la fois une signature de module et un module, c'est plus simple.
[^] # 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.
Dans les faits, la cohérence interne que tu peux vérifier est assez faible. Comme les gens détestent écrire les choses 2 fois, tu te retrouves à faire des calculs avec des données que tu as déjà, plutôt que vérifier que 2 valeurs sont cohérentes.
Pour l'exemple que tu donnes, cela tombe exactement dans ingénierie des modèles et le genre de petites règles que tu peux écrire. C'est très utile, tu peux augmenter très largement la productivité des utilisateurs. Mais tu ne vérifies pas de cohérence en soi, tu écris la règle elle-même. On est très loin d'une "vérification formelle".
"La première sécurité est la liberté"
[^] # 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.
J'ai un peu trop divergé je suis d'accord.
Pour ça, il faut un "modèle du monde", ce qui n'existe jamais. C'est le boulot de dingue qui consiste à modéliser toutes les instructions assembleur dans compcert. Donc, non, tu n'as rien de facile sous la main pour confronter ce qu'écrit une personne du métier. Ce qui est typiquement fait, c'est d'utiliser des simulateurs maisons ou pas. Une équipe du métier conçoit un nouveau logiciel de pilote automatique, il va simuler des scénarios pour le valider. Il n'y a pas de règles statiques pour valider qu'il fait n'importe quoi dans certain cas. Dans le cas de ingénierie des modèles, on peut toujours écrire des règles qui permettent de vérifier certaine propriété, c'est forcément limité.
L'autre info c'est de voir le renforcement de alphagoZero en jouant contre lui-même en simulant des parties. Il devrait en théorie être possible de faire une IA qui apprend en utilisant un simulateur. C'est très théorique, je suis d'accord, mais cela serait la porte d'entré de l'IA dans l'ingénierie.
"La première sécurité est la liberté"
[^] # 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é à 4.
Oui, c'est la merde pour ça. Je code avec gokit, et je souffre.
ex: https://github.com/go-kit/kit/blob/master/examples/shipping/routing/proxying.go
Il y a 36 wrappers à écrire pour masquer les interface{}.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
J'imagine qu'au final, leur GC est 20% plus lent que l'ancien. Je ne retrouve l'article sur le gc 1.9.
Ils en parlent un peu ici : https://golang.org/doc/go1.9
"La première sécurité est la liberté"
[^] # 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.
Le "modèle métier" se confronte toujours à une simulation. D'ailleurs, j'imagine qu'un jour les IA s'amuseront directement avec ce genre de simulateur.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Par exemple, le GC de go 1.9 fait maintenant des pauses maximum de 9 ms et utilise des threads. Mais il prends un peu plus de temps cpu pour vérifier la totalité de la RAM. Cela veut dire que pour un serveur chargé qui marche bien actuellement, le nombre de transaction par seconde risque de baisser, même si la latence moyenne pour chaque requête baisse.
"La première sécurité est la liberté"
[^] # 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.
Je pense que pour vraiment se passer de interface{}, il faudrait de l'inférence de type à la place, ce qui n'est pas gagné.
"La première sécurité est la liberté"
[^] # 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é à 4.
Dans l'outil d'ET, il y a un prouveur qui marche assez bien (surtou avec les machines d'état). Je lui est déjà fait trouver des contres-exemples, mais personne ne l'achète ni ne s'en sert.
"La première sécurité est la liberté"
# Question bête
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche LibraZiK : nouveautés des six derniers mois. Évalué à 9.
Pourquoi faire une Debian dédié plutôt qu'un metapackage qui regroupe tous vos choix ?
"La première sécurité est la liberté"
[^] # 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é à 1.
Le bug peut être également dans le model. J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
J'ai entre autre appris, que les spécialistes métiers ne sont pas des informaticiens et encore moins des matheux. Et que pour décrire leur système, ils ne veulent surtout pas avoir à faire à ce genre de concept. Ils veulent pouvoir décrire des problème spécifique, les exemples de why3 dont parlait mon commentaire, n'ont aucun rapport avec des problèmes industriels.
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier. C'est le sujet du journal.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
"La première sécurité est la liberté"
[^] # 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.
Dans un vieux journal, je parlais d'un langage que j'ai tenté décrire suivant la mode des langages systèmes, un truc qui ressemble a du xml mais avec une notion de nommage pour faire des graphs acycliques. Le truc est mal définit mais bon. Je me demandais si il n'était pas plus sage d'utiliser un truc costaux comme coq ou pourquoi pas why3 pour vérifier le fichier au lieu de le faire à la main. L'idée est d'avoir un langage structurel très user-friendly, dont la vérification est sous traité. L'idée est qu'un langage structurel est plus facile à vérifier.
"La première sécurité est la liberté"
[^] # 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.
compcert a été prouvé avec seulement ce bout de code ? Sans rien de manuel ?
Pour info, j'ai bossé 10 ans dans l'aéronautique, et l'usage des compilos C certifié c'était plutôt : "il faudrait prendre le temps de voir ce que cela donne". De plus la preuve formelle n'est pas encore reconnu dans les certifications aéronautique, en tout cas dans la do178b, je crois que cela bouge un peu dans la DO178C. Et encore, j'imagine que le prouveur lui-même devrait être certifié… Donc, on est pas prêt de voir un avion volé avec un tel code sans certification "papier" à coté. L'outil de ma boite utilisait l'outil de prover, mais c'était peu/aps utilisé car la norme n'en voulait pas.
Je crois que je peux te répondre la même chose, mais pas pour le même domaine.
"La première sécurité est la liberté"
[^] # 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.
Tu crois que cela ressemble à quoi des vrai spec ? :) Je faisais un référence un peu trop subtile à un défaut d'un cruise control de toyota qui s'est fait démonté par un expert aéronautique pour un procès : il ne se désactivait pas si la pédale de frein était enfoncé…
En gros, cela voudrait dire que quelques soit les autres entrés, l'arrivé de l’arrêt d'urgence doit arrêter les moteurs.
Je sais bien, c'est d'autant plus difficile que le langage de la preuve est éloigné du langage métier, ou du langage de dev.
"La première sécurité est la liberté"
[^] # 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. Dernière modification le 20 octobre 2017 à 15:38.
Je parlais du site web de why3. ( http://toccata.lri.fr/gallery/why3.en.html )
Concernant le code du drone, on dirait qu'il a seulement fait attention au overflow de calcul. Il faut que je relise moins en diagonal, je n'ai pas vu de propriété spécifiquement vérifier (genre l’arrêt d'urgence fonctionne dans tous les cas).
http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark regardes le 2ième commentaires qui signale tout un tas de problème dans les specs du truc.
"La première sécurité est la liberté"
[^] # 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. Dernière modification le 20 octobre 2017 à 14:55.
Les exemples de preuve sont très matheux. Cela ne ressemble pas à des preuves "industrielles" (à base de bout de spec, de bout d'exemple, de ne "plante jamais", a un temps d'exécution borné).
"La première sécurité est la liberté"
[^] # 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é à 2.
Plein de choses :
- ton exemple n'a rien à voir avec un truc réel. Je parlais de typage statique, le genre de truc que l'on trouve dans ocaml, qui ne permet pas ce que tu écris.
- ton exemple n'a jamais été passé dans un prouveur automatique, la démo est manuelle (frama-c ?)
- il faut que l'expressivité soit compréhensible par le commun des mortels, why3 a l'air sympa comme coq, mais il faut être un matheux pour s'en servir. frama-c est un sous ensemble du C, et n'est même pas optimisant !
- c'est très rare d'avoir une spécification aussi simple, un compilo qui optimise, on compare le comportement de sa génération de code sans optimisation, et on colle un fuzzer devant. Imagines le bordel de convertir 500 HLR dans ce genre de langage.
- pour avoir bosser avec un prouveur, l'idéal est de pouvoir écrire un truc dans le même langage et lui demander si la sortie est toujours vrai. Dans le cas contraire, il fournit un contre-exemple. C'est juste énorme. En général, il répond qu'il ne sait pas faire.
"La première sécurité est la liberté"
[^] # 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é à 4.
Il y a un rapport entre why3 et coq ?
"La première sécurité est la liberté"
[^] # 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é à 2.
Le problème est que tu n'attrapes pas grand chose comme erreur avec un système de typage. La seul architecture que j'ai trouvé pour aider est de transformer un arbre en un autre, sans aucune information redondante ni inutile. Ainsi, un mauvais usage ne compile pas, et on ne traine pas l'entrée à l'intérieur du code. Cela marche bien dans les "filtres unix" mais dans rien d'autre, pour des raisons de performances si les données sont énormes ou pour des raisons pratiques comme l'optimisation d'un AST qui doit donner aussi un AST.
Si on regarde le gadt, la complexité est encore plus grande sans réellement attraper une énorme quantité de bugs supplémentaires. En gros, la complexité devient exponentielle, pour attraper des bugs de façon linéaire.
J'ai discuté avec l'auteur français de smarteffel(?), qui utilise beaucoup les contrats, il disait qu'en codant, il violait régulièrement même des contrats de base présent dans les containers, car la pile d’héritage en bénéficiait (les contrats n’héritent). C'était d'une grande aide pour lui.
Le problème est que le contrat est runtime et nécessite un test pour s’exercer. Il n'est pas possible d'avoir des contrats compile-time ou de vérifier leur cohérence entre eux ?
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3. Dernière modification le 20 octobre 2017 à 10:18.
Attention, la concision est souvent l'ennemi de la clarté. VHDL et ADA sont très verbeux mais très lisible. Je pense que l'abus de symbole est horrible pour la lecture. L'exemple typique sont les regexp Perl qui sont un cauchemar à lire, mais pas à écrire.
Je me demande même si les symboles ne prennent pas "plus de place" dans la tête car il ne se prononce pas, sauf les symboles de base (+).
Pour moi, ce truc est bizarre car 2 mots clef se suivent ce qui est très rare ("Module type"), ensuite je lit "M = sig", sig étant un mot clef et ne m'indique pas du tout le début d'une liste qui se fait d'habitude avec des '(' ou des '{' ou des '[' voir des '<'. Ensuite, il y a le ':' qui alourdit la notation, alors que ocaml est ultra light d'habitude (pas de ',', ni de '(').
En go, cela donnerait :
type M module {
type t
var v t
}
C'est génial ça, il existe un autre langage où c'est possible, ou c'est impossible à compiler ?
Tu te rends compte qu'en go, cette fonctionnalité se fait simplement avec une fonction String() dans un objet ? Elle est reconnu comme présent dans la bonne interface, et le tour est joué.
type Stringer interface {
String() string
} // est définit dans le code du package fmt
Non, elles ne sont pas proche justement, ni symétrique.
C'est le but. Coq lui même ne fait pas la différence entre type et valeur, et c'est plus simple.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Le temps de re-rentrer dans du code perdu de vue depuis longtemps est un très bon moyen d'évaluer l'ergonomie d'un langage, je trouve :)
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Pas mal. C'est simple, un type remplacer par génération, et élégant avec le code générique qui compile de base.
D'ailleurs, cela permet de voir la tonne de code généré si on s'amuse avec des modules génériques.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Je trouve la généricité, les modules très utile. Mais je trouve que leur forme dans ocaml est très complexe et très peu lisible. Cela parait peut être évident pour toi qui est tombé dedans que tu es petit. Mais pour un concept complexe, il faut qu'il ressemble le plus possible à quelques choses de connu (principe UX de moindre surprise). Les modules ressemblent ici vaguement à des objets, avec des définitions de type dedans, mais avec une autre syntaxe.
En fait, je pense qu'il doit être possible de proposer des modules en GO mais avec une syntaxe ultra simplifié pour la compréhension.
Genre :
package toto (type t, int i)
func sort(tab t[i]) {…
import "toto"(int, 1024) -> l'idéal serait d'avoir un seul module instancié pour ce couple de paramètre
Pour l’extension d'un package, j'imagine qu'il doit y avoir déjà l'équivalent d'un "open".
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 5.
En fait, je pensais au cas d'usage qui reviennent au même. Dans l'esprit, c'est 3 façon d'écrire la même chose, c'est anti-ergonomique, même si c'est formel.
let rp : pt_2D = {x = 1.0; y = 2.0}
let op : obj_pt_2d = object method x = 1.0 method y = 2.0 end
module MP : mod_pt_2D = struct let x = 1.0 let y = 2.0 end
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 4.
Franchement écrit une proposition propre sur les type sum et poste un lien sur le blog de go 2.0
https://github.com/golang/go/wiki/ExperienceReports
Ils veulent des exemples, et nous on voudrait les types sum. Ils manquent sans doute une bonne explication entre les 2.
L'idéal serait de faire la même chose pour transformer les packages en module, en rajoutant une déclaration "parameter" pour définir des paramètres à remplir à l'import d'un package ou simplement d'ajouter une liste de paramètre à la déclaration de package, puis de fixer un moyen de créer des package "complet" avec ses paramètres. Cela évite un peu la duplication de code, si l'instanciation est faite une seul fois. Si la syntaxe de ces paramètres est exactement symétrique avec des paramètres de fonction, cela devrait rester simple. Il reste la création de signature de package dont je ne vois pas trop à quoi il pourrait ressembler en go. L'idéal serait qu'un package soit à la fois une signature de module et un module, c'est plus simple.
"La première sécurité est la liberté"
[^] # Re: go 2.0
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
tu devrais lire le lien sur la discussion sur les types sum.
Il demande par exemple comment filtrer "int | interface{}" sachant que interface{} fonctionne pour tout.
"La première sécurité est la liberté"