Thomas Douillard a écrit 9164 commentaires

Il faut peut-être juste un téléphone compatible, pas forcément la connexion Internet activée ?

Oui ça se fait, c'est assez lourd. J'imagine que ça se justifie de pas s'encombrer avec ça si c'est "suffisamment bon" sur toutes les plateformes.

Tu peux vouloir mettre au point pour que ce soit optimal sur des plateformes différentes ?

Il y a pas de calques dans les png. Donc si tu fermes ton logiciel, tu les perds automatiquement. Faut pas avoir de regrets après coup sur le résultat.

Je ne me sens pas rabaissé personnellement, je me dis juste qu’Ada Lovelace, à force de la donner en exemple son nom va finir par être un peu reconnu.

Après j’ai conscience qu’en tant que geek j’ai probablement une connaissance plus poussée de ces sujets que la plupart des gens et de vivre un peu dans une bulle comme tout le monde, et je trouve plus passionnant comme débat d’autres choses que de s’offusquer du titrage de ce genre d’article, donc je vais arrêter là.

Disons qu’à force de faire ce genre d’articles et autres œuvres comme « les femmes de l’ombre » certains des noms commencent doucement à rentrer dans la tête du public … après certains geeks en savent plus que les autres mais ça (doit?) reste(r) la portion congrue de la population ?

Si on compare les statistiques de consultations de Wikipédia sur quelques personnes sur les quelques derniers mois:
* https://pageviews.wmcloud.org/?project=fr.wikipedia.org&platform=all-access&agent=user&redirects=0&start=2021-05&end=2022-04&pages=Ada_Lovelace|Albert_Einstein|Cyril_Hanouna|Hedy_Lamarr|Alan_Turing|Elvis_Presley|Mary_Wickes|Stephen_Cook

J’ai pris un noms connus de pop culture, un animateur contemporain, un chercheur inconnu du grand public mais qui a donné son nom à un théorème d’informatique théorique, quelques noms de l’articles, et Alan Turing qui a fait la une des journaux et fait l’objet de biopics assez récemment.

Stephen Cook est le moins consulté, bien qu’il soit encore vivant mais sans trop de surprise vu qu’il est pas mis en avant dans les médias, avec environ 50 vues, à l’autre extrême on a Hanouna et Einstein avec 75 000 et 70 000 vues mensuelles environ, suivi d’Elvis avec 50 000. Ensuite on a Turing avec 30 000, Hedy Lamarr avec 13 000, et Ada Lovelace avec 12 000. Mary Wickes ensuite avec 600, 10 fois plus de consultations que Cook

Il semble que des gens comme Cook sont aussi consultés que des gens comme notre première ministre avant sa nomination, je vous laisse juge de savoir si ça qualifie pour qualifier de « que personne ne connait » :p

Pourquoi ? C’est pas si simple de trouver la bonne requête à faire sur Internet et trier / traîter les résultats …

Le réveilleur avait fait une vidéo là dessus, en prenant l’hypothèse d’une voiture pas trop grosse : https://www.youtube.com/watch?v=zjaUqUozwdc

J’imagine qu’il suppose que si tu utilises ta connexion 5G tu abandonnes ta box ou tu l’allumes 3 minutes tous les 10 jours …

Si on se contentait de changer les appareils pour de plus efficaces, on diminuerait le nombre de datacenter, on ne l’augmenterait pas.

cela ne marche pas comme ça. C'est l'obsolescence qui fait changer les appareils qui sont bien plus efficace.

Et pourtant, on ne fait pas tout à nombre de datacenter constant, loin de la … https://www.usinenouvelle.com/article/les-geants-d-internet-ont-double-leur-nombre-de-datacenters-en-cinq-ans.N1140207

Et si tu évacues qu’il intègre la question des usages des technologies, tu rates toute une partie de son discours.

Ça a l’air raccord avec ce que dit le billet critique de la conférence cité par le journal https://airloren.github.io/devoxxfr/retour-conf-adam-beyssac/ , il faut des données. Mais il met l’accent sur avoir une bonne vision des ordres de grandeur avant de faire du microbenchmark.

Tu as l’air de vouloir opposer mail à vidéo mais … https://www.femmeactuelle.fr/vie-pratique/high-tech/comment-envoyer-une-video-par-mail-2083596 on en est plus à l’ère du mail ascii ?

Ça ne pose pas de problème pour les classes au sens mathématique du terme, il me semble. Le principe c’est justement qu’on peut utiliser n’importe quel prédicat sur une classe propre ?

Le truc pour ne pas avoir de paradoxe en théorie des ensembles c’est que tu ne peux pas statuer de « l’appartenance » d’une classe propre à une autre classe propre, et a fortiori à un ensemble. Si tu ne fais jamais ce genre de truc j’avoue que je vois pas trop en quoi il y aurait un problème à avoir n’importe quel prédicat. C’est juste que si ça laisse tout passer il y a des chances qu’une fonction avec un paramètre d’un tel type ne peut pas supposer grand chose.

https://fr.wikipedia.org/wiki/Classe_(math%C3%A9matiques)

Et aussi, si on étend, comment on considère que c’est OK d’additionner des nombres complexes avec des flottants ?

Dans ce cas tu attaches bien plus d’importance aux étiquettes de type que tu veux bien le croire, vu qu’un type ne peut être un sous-type d’un autre que s’il est spécifié comme tel. Alors que si tu veux démontrer des choses, tu pourrais partir sur une vérification non nominale que toutes les valeurs d’un type respectent le prédicat de validation d’un autre sans que ce soit explicitement écrit par sous-typage explicite.

Ton assert est donc totalement synonyme d’un truc style

class six(a: int) { n=6 }

a : six = add_five(1) ;

Ça amène a une question : tu typecheck dans ton document uniquement les paramètre des fonctions. En principe on vérifie que toutes les instructions typecheckent ?

Tu peux dans ce cas probablement définir un type unique de la manière suivante : le type de ton objet est le type de l’intersection de toutes les spécification des types qu’il peut remplir.

la constante 8 serait alors l’intersection des types int, even et mod4, donc de type mod4 puisque c’est un sous type strict des 2 et que even est un sous type de int.

Ça signifie que 8 peut être utilisé à la fois partout ou on attend un entier, un nombre pair ou un multiple de 4.

Mais ce n’est valable que sur les constantes non ?

Si tu as des fonctions style :

func f(four: mod4) -> { … }

func plop(a : int) -> int {
  b : int = 8 * a
  f(b)
}

ça typecheck ou tu comptes vérifier ça à l’exécution ?

C’est un système de typage nominal alors finalement. Le type est déterminé par le fait que tu ait fait passer la valeur par un constructeur du type, du coup tu peux lui coller l’étiquette « entier ». Si tu as une valeur de type nombre dont il serait possible avec un démonstrateur qu’elle est nécessairement un entier, elle ne sera pas déterminée comme tel comme ça pourrait l’être avec un système structurel de type (le type n’est pas donné par une étiquette de type mais par la forme/les propriétés de l’objet, cf. Système_structurel_de_types ). C’est quelque chose qui est assez classique en typage finalement, un constructeur d’un type apporte une preuve que certaines propriétés du type sont bien garanties. Un constructeur d’un type « liste triée » par exemple pourrait appliquer un tri sur une liste non triée en garantissant que le résultat est bien trié, et la propriété est garantie dans le système de type parce que la liste a bien le type « liste triée », qui permet de tracer la propriété finalement.

Tu dois avoir des « constructeurs » qui garantissent qu’une valeur de ton type a bien les bonnes propriétés. Et « int » ici c’est un sous-type de nombre dans le sens ou tu peux mettre un « int » dans n’importe quel contexte ou tu peux mettre un nombre, avec une relation de sous-typage qui est explicitement spécifiée. cf. Principe de substitution de Liskov.

C’était pas ma question, c’était surtout, dans le cas a // b comment tu garantis que a et b sont bien des entiers ?

A priori si tu définis simplement le fait d’être un entier par un prédicat sur le fait d’être un nombre, n’importe quel nombre pourrait être candidat à une division euclidienne. Le truc pour que ça marche c’est que tu dois être capable de garantir que ce nombre respecte bien ce prédicat ?

Et ça se passe comment si tu veux faire concrètement des calculs sur les variables entières ?

Genre la division entière, tu comptes t’y prendre comment ? Les opérandes sont des entiers et ça retourne un entier ou des nombres quelconques et tu dois garantir d’une manière ou d’une autre que le prédicat « frac(n) = 0 » est vrai ?

Sinon partie terminologique, tu parle de « part of the class », traditionnellement une partie c’est pas du tout un élément d’un ensemble mais un sous-ensemble, si tu veux être sur la théorie des ensembles. ça porte à confusion.

calcul des constructions ?

Si tu ne mets que les polynômes tu ne retrouves pas ton compte mais juste les Nombre_algébrique. Les nombres algébriques sont dénombrables, il existe un algorithme infini qui peut lister tous les polynomes, et chaque polynome a un nombre fini de solutions. Du coup comme on sait par l’Argument_de_la_diagonale_de_Cantor que les nombres réels ne le sont pas, dénombrables, on a pas assez de solutions polynomiales pour avoir tous les réels.

Les réels sont encore plus grands, on les trouve soit avec des coupures de Dedekin, c’est à dire l’ensemble des manières de découper les rationnels en deux partitions telles que tous les éléments d’une partition sont inférieurs à tous les autres, soit avec des suite de Cauchy, comme des limites de suites de rationnels qui convergent vers un truc. Ce truc étant un nombre réel.

D’autant plus qu’on peut faire des maths pas seulement dans la théorie des ensembles, mais aussi dans la théorie des types.

Les assistants de preuves comme Coq ou Lean qui a fait récemment parler de lui, cf. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ par exemple sont basés sur des théories des types. Les théories des types sont un sujet de recherche actif du point de vue mathématique, et pas seulement pour les maths-infos mais aussi pour des choses purement mathématiques. Cf. la théorie homotopique des types dont il a déjà été question ici je crois.

Si on travaille dans la théorie des ensembles un meilleur exemple pour montrer l’ambiguité serait peut être de parler de l’ensemble vide : il peut représenter assez naturellement … l’élément neutre de l’opération d’union de la théorie des ensemble, mais aussi si on code des nombres il peut coder le nombre 0 dans les entiers naturels dans la construction classique.

Mathématiquement 0 et l’ensemble vide sont bien évidemment des objets totalement différents, en théorie des ensembles, si on applique les axiomes et le codage classique des entiers naturels, ils sont … égaux (deux ensemble sont égaux si ils ont les même éléments).

C’est souvent un exemple d’absurdité qui est utilisé pour introduire la théorie des types aux mathématiciens qui sont habitués à travailler avec la théorie des ensembles. Le truc à noter c’est qu’en choisissant un autre codage des entiers naturels dans la théorie des ensembles le paradoxe disparait (mais d’autres pourraient apparaitre). Tout dépend de comment on choisit de coder les objets sur lesquels on veut travailler.

Je pense que ce qui pourrait manquer à la présentation, également, c’est une définition de ce que sont les « objets ». Ils sont pas introduits ni définis dans la présentation actuellement. Et il semble y avoir une confusion entre « objet » et « littéral » : le littéral « 5 » peut être utilisé pour représenter l’entier naturel 5 dans le code d’un programme. L’entier naturel a naturellement un type, par contre les littéraux c’est à définir. On peut très bien convenir que dans un contexte de calcul vectoriel ou sur les flottants on donne au littéral « 5 » d’autre significations … Et soit interprétés comme deux objets (dans le sens de valeur manipulées par le langage, des valeurs que peuvent prendre les variables) différents.

Dernier point sur le paradoxe de Russel : en quoi est-ce un problème en pratique ? Les classes pourraient être manipulables en tant que valeur du langage (« objet ») sans avoir la possibilité que le langage soit assez puissant pour pouvoir définir une collection de ces valeurs. Si tu veux avoir des variables « non déterministes » qui pourraient avoir comme valeur plusieurs « objet classes » possibles ça doit pouvoir rester possible en faisant attention à ce que cet ensemble de classe soit « fermé », ou alors faire en sorte que les variables qui contiennent des classes soient « déterministes » dans le sens ou il ne peuvent avoir qu’une seule valeur possible.