La façon de comprendre la traduction entre de “truth” et “falsity” en termes de CS “type singleton” et “type vide” est que “A implique B est vraie” et “il existe une et une seule fonction de A vers B”, correct?
Hum, ta phrase est un peu bancale grammaticalement et je ne comprends pas très bien où tu veux en venir. Je peux te justifier la définition calculatoire de « vrai » et « faux » comme suit. Il y a une et une seule preuve de « vrai », et donc « vrai » est l'équivalent sur le versant logique du type unit d'OCaml, disons (tu as l'air de pratiquer), i.e. le type algébrique à un seul constructeur (type unit = ()). De la même manière, on espère secrètement qu'il n'y a pas de preuve de faux, donc on définit faux comme le type vide, i.e. le type algébrique à zéro constructeurs (je ne crois pas que ça soit possible en OCaml pour des raisons débiles de parsing, mais tu peux l'encoder avec des GADTs).
Est-ce qu'il n'y a pas un poly que tu pourrais me recommander. Je suis mathématicien mais je ne suis pas très familier avec le domaine de la logique proprement dite ou la théorie des types, donc je pense que je pourrais arriver à profiter un peu d'un cours de DEA ou de Master.
Si tu aimes les catégories, tu peux tenter le HoTT book, même si je dois avouer que ne cautionne pas l'OPA qu'ont fait les homotopistes sur la théorie des types et le rebranding en « homotopique » de plein de choses qui existaient déjà dans la bête théorie des types. À part ça, dans la catégorie « bouquin moderne », je vois pas trop. Type Theory and Functional Programming a l'air pas trop mal à vue de nez.
D'ailleurs, j'ai l'impression que ta compréhension de ∃x : A. P[x] est aussi un peu biaisée. Un programme de type ∃x : A. P[x] est une paire (t, p) faite d'un programme t : A et d'un programme p : P[t]. C'est la magie de la correspondance de Curry-Howard. Je me permets de mettre un lien vers des slides introductives à moi sur le sujet.
Du coup je n'ai pas trop d'intuition sur la taille des programmes qu'on peut pratiquement prouver avec coq.
Les trucs publics les plus gros sur le versant informatique que je connaisse en Coq sont Compcert et Bedrock, respectivement un compilateur C prouvé et un cadriciel de preuve de programmes. Bon, en pratique les limites de la scalabilité en Coq ne sont pas trop là où on s'attend, et des problèmes pratiques débiles te sautent à la figure avant d'atteindre des frontières techniques.
par contre pour transformer le pour tout en logique intuitionniste, j'ai moins fait le malin
Je vois pas très bien ce que tu veux dire. Un terme de type ∀x : A. P est une fonction prenant en argument un terme t de type A et renvoyant du P[t]…
C'est drôle, je viens tout récemment d'entendre parler de ces gens-là, qui font des gros systèmes distribués en se reposant sur la programmation fonctionnelle (surtout du Haskell et du OCaml, semble-t-il). Et le site, quoiqu'un peu vide, indique qu'ils recrutent…
Les trucs vraiment théoriques, genre la théorie des catégories (foncteurs, monades, types algébriques)
Je me permets d'interrompre ce flil parce qu'on se fout un peu de notre gueule : dire que les types algébriques sont des trucs vraiment théoriques, c'est soit de l'ignorance crasse, soit de la mauvaise foi mielleuse. À ce compte-là, autant prétendre que les structures de données c'est compliqué, ou qu'on peut tout écrire en TeX.
Les types algébriques sont simples à la fois à comprendre et à implémenter, et permettent un saut expressif monstrueux comparé au coût de leur introduction. Je pleure toujours d'amères larmes en constatant qu'en 2015, aucun langage mainstream ne les propose (mais c'est en train de changer).
Ça me fait penser à un truc que je n'ai pas cité dans la dépêche, mais qui est un phénomène bien connu chez les utilisateurs d'assistants de preuve.
Il est clair que prouver formellement est difficile, mais ça a un côté jeu vidéo très addictif. En particulier, je connais pas mal de gens qui sont capable de passer des heures sur Coq afin de venir à bout d'un théorème. Il semble clair que cela est provoqué par l'interactivité des prouveurs, qui ont un air certain de point-n'-click. Je connais même des gens qui se font réprimander pour avoir passé trop de temps sur Coq…
Bref, les preuves formelles, contrairement à ce qu'on pourrait croire, c'est marrant. Et à coup sûr plus fascinant que Flappy Bird.
D'ailleurs, on vient tout juste de brancher la version 8.5 de Coq, et avec la quantité de récompenses reçues par Coq l'année dernière, je pense que c'est l'occase pour une petite dépêche pour sensibiliser les moules à la volaille !
Permettez-moi donc de faire une remarque de semantic nazi.
On ne dit pas « gouvernement » dans ce sens-là, ça sent bon les séries américaines mal traduites. Le gouvernement, ce sont les ministres et leur conseillers. Ici, on parlera plutôt d'administration.
Dans le même genre poussé à l'extrême, il y a l'équipe de Georges Gonthier de chez Microsoft Research qui a prouvé le théorème des quatre couleurs et le théorème de Feit-Thompson en Coq… Deux réussites monstrueuses des mathématiques assistées par ordinateur ! Pas grand chose à voir avec Windows, heureusement.
Le site a l'air assez perché et me promet qu'Evenja va pouvoir réparer les motos russes à distance, mais il n'indique pas vraiment ce que c'est. Je n'ai pas très bien compris si c'était un paradigme de langage de programmation, ou bien de développement. Dans le premier cas, est-ce que c'est une forme de programmation réactive ?
Les overloads sont justement l'antithèse du polymorphisme paramétrique, ce qu'on appelle aussi polymorphisme ad-hoc, parce que les fonctions peuvent faire des choses très différentes selon leur type. Les templates présentent le problème cité dans l'article, à savoir une duplication de code à la compilation.
Pour prendre un équivalent de la fonction bsearch en ML, on pourrait imaginer une fonction
bsearch: 'a -> 'a list -> ('a -> 'a -> bool) -> 'a
où le premier 'a correspond à key, le 'a list correspond à base, la fonction ('a -> 'a -> bool) à compare et le derner 'a est le type retourné.
Ici, point de duplication de code, il n'y a qu'une seule fonction créée à la compilation. Le 'a joue ici le rôle du void* effacé, i.e. c'est un type universellement quantifié, sauf qu'en plus on a la type-safety au niveau des contraintes. Le code se comporte de manière uniforme sur tout les types, au contraire de l'overloading.
Avec de tels principes, les langages de programmation en seraient restés au COBOL…
Non, je suis désolé, mais TeX est un logiciel des années 70, et on le sent bien. Depuis on a fait des progrès dans la conception des langages de programmation, et des limitations arbitraires comme le fait de ne pouvoir avoir qu'au plus 256 variables font franchement préhistoriques.
Le fait de pouvoir créer des DSL de manière locale avec un métalangage, typiquement. J'ai souvent envie de parser puis manipuler des ASTs dans une présentation pour les enrichir à loisir et les afficher selon mon bon vouloir. Chose assez difficile à faire dans un langage comme TeX ou JS…
Je songeais moi aussi à utiliser HTML comme backend pour faire des présentations, parce que j'ai beau aimer le rendu de LaTeX, Beamer, c'est quand même assez arcanesque. Je précise quand même que je fais assez régulièrement des présentations en Beamer (je dois en faire une demain, d'ailleurs).
Le problème principal, commun à (La)TeX et HTML/Javascript, c'est leur langage de programmation, insupportable dans les deux cas. Javascript peut-être un peu plus expressif que TeX, il n'en reste pas moins que je préférerais un langage vraiment moins crade.
Je pense explorer deux pistes. D'une part, j'ai entendu du bien de quelques gusses de ma connaissance qui développent le langage de mise en forme du futur, j'ai nommé Patoline. Ils ont même un backend OpenGL pour faire des diagrammes 2-catégoriques en 3D qui tournent tous seuls, c'est dire.
L'autre méthode serait d'utiliser l'artillerie lourde à base d'Ocsigen pour générer du HTML à partir de code OCaml, et plus précisément js_of_ocaml, qui est un compilateur OCaml vers Javascript.
Oui, je précise aussi qu'OCaml est mon langage de préférence, qu'il se prête très bien au scripting, et que ces deux solutions utilisent précisément OCaml en interne. Je suis cependant preneur de n'importe quelle solution qui utiliserait un langage décent (exit JS donc).
Bof. Les robots korriganoïdes risquent d'être bien moins efficaces qu'un robot cubique moche mais fait exprès pour réparer des trucs dans l'espace.
Les Japonais semblent souffrir d'un complexe assez délirant vis-à-vis des robots, appuyé par le fait qu'il est quasiment impossible de posséder un animal de compagnie en ville. Pour moi, l'idée même du robot de compagnie est à peu près aussi inepte que celle des tamagochis. J'attends de voir le jour où la présence d'un tel robot sera au moins aussi agréable que celle d'un ornithorynque[1].
[1] Sous réserve que celui-ci ne boive pas vos bières dans votre dos.
[^] # Re: Le web
Posté par Perthmâd (site web personnel) . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 2.
Hum, ta phrase est un peu bancale grammaticalement et je ne comprends pas très bien où tu veux en venir. Je peux te justifier la définition calculatoire de « vrai » et « faux » comme suit. Il y a une et une seule preuve de « vrai », et donc « vrai » est l'équivalent sur le versant logique du type unit d'OCaml, disons (tu as l'air de pratiquer), i.e. le type algébrique à un seul constructeur (type unit = ()). De la même manière, on espère secrètement qu'il n'y a pas de preuve de faux, donc on définit faux comme le type vide, i.e. le type algébrique à zéro constructeurs (je ne crois pas que ça soit possible en OCaml pour des raisons débiles de parsing, mais tu peux l'encoder avec des GADTs).
Si tu aimes les catégories, tu peux tenter le HoTT book, même si je dois avouer que ne cautionne pas l'OPA qu'ont fait les homotopistes sur la théorie des types et le rebranding en « homotopique » de plein de choses qui existaient déjà dans la bête théorie des types. À part ça, dans la catégorie « bouquin moderne », je vois pas trop. Type Theory and Functional Programming a l'air pas trop mal à vue de nez.
[^] # Re: Le web
Posté par Perthmâd (site web personnel) . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 4.
D'ailleurs, j'ai l'impression que ta compréhension de ∃x : A. P[x] est aussi un peu biaisée. Un programme de type ∃x : A. P[x] est une paire (t, p) faite d'un programme t : A et d'un programme p : P[t]. C'est la magie de la correspondance de Curry-Howard. Je me permets de mettre un lien vers des slides introductives à moi sur le sujet.
[^] # Re: Le web
Posté par Perthmâd (site web personnel) . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 2.
Les trucs publics les plus gros sur le versant informatique que je connaisse en Coq sont Compcert et Bedrock, respectivement un compilateur C prouvé et un cadriciel de preuve de programmes. Bon, en pratique les limites de la scalabilité en Coq ne sont pas trop là où on s'attend, et des problèmes pratiques débiles te sautent à la figure avant d'atteindre des frontières techniques.
Je vois pas très bien ce que tu veux dire. Un terme de type ∀x : A. P est une fonction prenant en argument un terme t de type A et renvoyant du P[t]…
# Coïncidence
Posté par Perthmâd (site web personnel) . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 2.
C'est drôle, je viens tout récemment d'entendre parler de ces gens-là, qui font des gros systèmes distribués en se reposant sur la programmation fonctionnelle (surtout du Haskell et du OCaml, semble-t-il). Et le site, quoiqu'un peu vide, indique qu'ils recrutent…
[^] # Re: Saboteur 2
Posté par Perthmâd (site web personnel) . En réponse au journal Concours de musique 1-bit. Évalué à 2.
Je préfère personnellement celle-là, que je trouve bien catchy :
https://www.youtube.com/watch?v=9dYAx0h9e5Y
[^] # Re: Pas de publicité ?
Posté par Perthmâd (site web personnel) . En réponse au journal Et si la gratuité de Windows 10 n'était qu'un moyen pour déstabiliser Linux ?. Évalué à 1.
Qu'est-ce qui les empêche de faire ça via un protocole décentralisé type bittorent plutôt ? C'est fait pour…
[^] # Re: adéquation
Posté par Perthmâd (site web personnel) . En réponse au journal François Hollande visite 42, non mais allô quoi.... Évalué à 5.
Je me permets d'interrompre ce flil parce qu'on se fout un peu de notre gueule : dire que les types algébriques sont des trucs vraiment théoriques, c'est soit de l'ignorance crasse, soit de la mauvaise foi mielleuse. À ce compte-là, autant prétendre que les structures de données c'est compliqué, ou qu'on peut tout écrire en TeX.
Les types algébriques sont simples à la fois à comprendre et à implémenter, et permettent un saut expressif monstrueux comparé au coût de leur introduction. Je pleure toujours d'amères larmes en constatant qu'en 2015, aucun langage mainstream ne les propose (mais c'est en train de changer).
[^] # Re: À l'autre bout du spectre
Posté par Perthmâd (site web personnel) . En réponse au journal Enfin une solution pour du café libre au boulot.. Évalué à 1.
Il n'y a pas moyen de faire ça à pas cher avec une pompe à vide manuelle des familles ?
[^] # Re: Ha le Parti Socialiste...
Posté par Perthmâd (site web personnel) . En réponse au journal Puis ils sont venus me chercher, et il ne restait personne pour protester. Évalué à 4.
Les monopôles socialistes n'existent pas, ils sont de divergence nulle !
[^] # Re: Objectif, en pratique?
Posté par Perthmâd (site web personnel) . En réponse au journal Ming Tea. Évalué à 3.
KTurtle, c'est has-been, à l'époque du TaaS (Turtle as a Service), on fait ça dans son navigateur !
[^] # Re: Idris
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Sortie de Coq 8.5 bêta, un assistant de preuve formelle. Évalué à 10.
Ça me fait penser à un truc que je n'ai pas cité dans la dépêche, mais qui est un phénomène bien connu chez les utilisateurs d'assistants de preuve.
Il est clair que prouver formellement est difficile, mais ça a un côté jeu vidéo très addictif. En particulier, je connais pas mal de gens qui sont capable de passer des heures sur Coq afin de venir à bout d'un théorème. Il semble clair que cela est provoqué par l'interactivité des prouveurs, qui ont un air certain de point-n'-click. Je connais même des gens qui se font réprimander pour avoir passé trop de temps sur Coq…
Bref, les preuves formelles, contrairement à ce qu'on pourrait croire, c'est marrant. Et à coup sûr plus fascinant que Flappy Bird.
[^] # Re: Une autre approche est possible
Posté par Perthmâd (site web personnel) . En réponse à la dépêche [code] Trouver les erreurs. Évalué à 8.
D'ailleurs, on vient tout juste de brancher la version 8.5 de Coq, et avec la quantité de récompenses reçues par Coq l'année dernière, je pense que c'est l'occase pour une petite dépêche pour sensibiliser les moules à la volaille !
# Affreux anglicisme
Posté par Perthmâd (site web personnel) . En réponse au journal Il est temps que vous ayez un meilleur HTTPS. Évalué à 10.
Permettez-moi donc de faire une remarque de semantic nazi.
On ne dit pas « gouvernement » dans ce sens-là, ça sent bon les séries américaines mal traduites. Le gouvernement, ce sont les ministres et leur conseillers. Ici, on parlera plutôt d'administration.
Une note à ce sujet par nos cousins d'outre-Atlantique.
[^] # Re: ingénieur peu considéré en France
Posté par Perthmâd (site web personnel) . En réponse au journal Téléphoner à ma mère: gratuité, simplicité, liberté ou vie privée?. Évalué à 6.
Il n'y a plus de postes dans la recherche publique… Ce document est assez édifiant.
[^] # Re: les matheux aussi
Posté par Perthmâd (site web personnel) . En réponse au journal Unicode 7.0 is out. Évalué à 2.
Le terme technique est « collationner », je pense.
# Merci la preuve formelle
Posté par Perthmâd (site web personnel) . En réponse au journal OpenSSL : une nouvelle faille découverte permet une attaque de l'homme du milieu. Évalué à 6.
La faille a été trouvée en tentant de prouver OpenSSL en Coq :
http://ccsinjection.lepidum.co.jp/blog/2014-06-05/CCS-Injection-en/index.html
Vous savez ce qu'il vous reste à faire…
[^] # Re: un grand contributeur à l'algorithmique répartie
Posté par Perthmâd (site web personnel) . En réponse au journal Et le prix Turing revient à .... Évalué à 7.
Dans le même genre poussé à l'extrême, il y a l'équipe de Georges Gonthier de chez Microsoft Research qui a prouvé le théorème des quatre couleurs et le théorème de Feit-Thompson en Coq… Deux réussites monstrueuses des mathématiques assistées par ordinateur ! Pas grand chose à voir avec Windows, heureusement.
# RP
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Concours "Evenja Café", un nouveau paradigme de programmation. Évalué à 7. Dernière modification le 06 janvier 2014 à 13:05.
Le site a l'air assez perché et me promet qu'Evenja va pouvoir réparer les motos russes à distance, mais il n'indique pas vraiment ce que c'est. Je n'ai pas très bien compris si c'était un paradigme de langage de programmation, ou bien de développement. Dans le premier cas, est-ce que c'est une forme de programmation réactive ?
# Singularité
Posté par Perthmâd (site web personnel) . En réponse au journal Systemd va gagner une console système, un bootsplash et un login-screen. Évalué à 5.
Mais la vraie question, c'est de savoir quand on va atteindre la singularité : le jour où systemd aura plus de features que Gnome, et réciproquement.
[^] # Re: Il serait peut-être temps d'utiliser des langages modernes
Posté par Perthmâd (site web personnel) . En réponse au journal Si si, le C++ peut parfois être plus rapide que le C. Évalué à 8.
Les overloads sont justement l'antithèse du polymorphisme paramétrique, ce qu'on appelle aussi polymorphisme ad-hoc, parce que les fonctions peuvent faire des choses très différentes selon leur type. Les templates présentent le problème cité dans l'article, à savoir une duplication de code à la compilation.
Pour prendre un équivalent de la fonction bsearch en ML, on pourrait imaginer une fonction
où le premier 'a correspond à key, le 'a list correspond à base, la fonction ('a -> 'a -> bool) à compare et le derner 'a est le type retourné.
Ici, point de duplication de code, il n'y a qu'une seule fonction créée à la compilation. Le 'a joue ici le rôle du void* effacé, i.e. c'est un type universellement quantifié, sauf qu'en plus on a la type-safety au niveau des contraintes. Le code se comporte de manière uniforme sur tout les types, au contraire de l'overloading.
# Il serait peut-être temps d'utiliser des langages modernes
Posté par Perthmâd (site web personnel) . En réponse au journal Si si, le C++ peut parfois être plus rapide que le C. Évalué à 6.
C'est moi ou ce que cet article décrit n'est rien d'autre qu'une implémentation hackish au possible du polymorphisme paramétrique ?
Genre, ML le faisait dans les années 70…
« Mauvais langage, changer langage ? »
[^] # Re: Langage
Posté par Perthmâd (site web personnel) . En réponse au journal Le HTML (epub3) peut il détrôner latex (surtout beamer) ?. Évalué à 8.
Avec de tels principes, les langages de programmation en seraient restés au COBOL…
Non, je suis désolé, mais TeX est un logiciel des années 70, et on le sent bien. Depuis on a fait des progrès dans la conception des langages de programmation, et des limitations arbitraires comme le fait de ne pouvoir avoir qu'au plus 256 variables font franchement préhistoriques.
[^] # Re: Question intéressante
Posté par Perthmâd (site web personnel) . En réponse au journal Le HTML (epub3) peut il détrôner latex (surtout beamer) ?. Évalué à 1.
Le fait de pouvoir créer des DSL de manière locale avec un métalangage, typiquement. J'ai souvent envie de parser puis manipuler des ASTs dans une présentation pour les enrichir à loisir et les afficher selon mon bon vouloir. Chose assez difficile à faire dans un langage comme TeX ou JS…
# Question intéressante
Posté par Perthmâd (site web personnel) . En réponse au journal Le HTML (epub3) peut il détrôner latex (surtout beamer) ?. Évalué à 2. Dernière modification le 21 octobre 2013 à 23:42.
Je songeais moi aussi à utiliser HTML comme backend pour faire des présentations, parce que j'ai beau aimer le rendu de LaTeX, Beamer, c'est quand même assez arcanesque. Je précise quand même que je fais assez régulièrement des présentations en Beamer (je dois en faire une demain, d'ailleurs).
Le problème principal, commun à (La)TeX et HTML/Javascript, c'est leur langage de programmation, insupportable dans les deux cas. Javascript peut-être un peu plus expressif que TeX, il n'en reste pas moins que je préférerais un langage vraiment moins crade.
Je pense explorer deux pistes. D'une part, j'ai entendu du bien de quelques gusses de ma connaissance qui développent le langage de mise en forme du futur, j'ai nommé Patoline. Ils ont même un backend OpenGL pour faire des diagrammes 2-catégoriques en 3D qui tournent tous seuls, c'est dire.
L'autre méthode serait d'utiliser l'artillerie lourde à base d'Ocsigen pour générer du HTML à partir de code OCaml, et plus précisément js_of_ocaml, qui est un compilateur OCaml vers Javascript.
Oui, je précise aussi qu'OCaml est mon langage de préférence, qu'il se prête très bien au scripting, et que ces deux solutions utilisent précisément OCaml en interne. Je suis cependant preneur de n'importe quelle solution qui utiliserait un langage décent (exit JS donc).
[^] # Re: Secours.
Posté par Perthmâd (site web personnel) . En réponse au journal Un robot sur la station spatiale. Évalué à 9.
Bof. Les robots korriganoïdes risquent d'être bien moins efficaces qu'un robot cubique moche mais fait exprès pour réparer des trucs dans l'espace.
Les Japonais semblent souffrir d'un complexe assez délirant vis-à-vis des robots, appuyé par le fait qu'il est quasiment impossible de posséder un animal de compagnie en ville. Pour moi, l'idée même du robot de compagnie est à peu près aussi inepte que celle des tamagochis. J'attends de voir le jour où la présence d'un tel robot sera au moins aussi agréable que celle d'un ornithorynque[1].
[1] Sous réserve que celui-ci ne boive pas vos bières dans votre dos.