thoasm a écrit 9443 commentaires

Bug rapporté ?

Ici tu confonds deux choses : la logique du premier et la logique intuitionniste. La première concerne les règles de formation des jugements, la seconde traite des règles d'inférences ou raisonnements.

Mmm après réflexion je dirai plutôt que je fais une erreur stupide : je confonds implication et déduction. Par définition, une logique s’intéresse aux règles de constructions et à la formation des jugements … La non constructivité induit qu’il n’existe pas forcément de moyen de former un algorithme à partir du théorème ou de la formule, et c’est bien tout … Je crois que tu confonds « formule de la logique du premier ordre » et « logique du premier ordre ». Ou alors c’est moi qui confond … Parce que dans mon esprit, la logique du premier ordre est un système formel, donc comprend les règles de déduction : https://en.wikipedia.org/wiki/First-order_logic (et wp semble être d’accord avec moi) ou alors j’ai rien compris à ce que tu dis :) La logique intuitionniste est aussi un système de déduction, mais avec des règles de déduction différente. Ou alors tu voulais dire « la logique intuitionniste du premier ordre est l’archétype du typage dynamique » ?

Du coup je me fourvoyai effectivement, tu parlais à chaque fois de système de déduction intuitionnistes. Tu établis 'une correspondance preuve/programme qui ne fonctionne que pour ces système, et je pensai que tu associais un système non intuitionniste pour les langages dynamiques. Alors que tu établies plus une distinction théorie à variable typée/théorie à variable pas typée.

Cela dit j’ai quand même l’impression d’être grugé. Dans un cas, le connecteur « -> » est vu par correspondance de curry-howard comme le type d’une fonction, alors que dans l’autre pour un langage dynamique tu as complètement oublié cette correspondance implication/fonction et c’est le quantificateur qui joue ce rôle.

Sinon t’embêtes pas trop sur le Kantisme, j’ai parcouru les articles sur « noumène et phénomène » de la wp en anglais, qui sont instructifs et mettent bien en lumière les difficultés d’interprétation. , j’en conclu que tout tourne autour du thème « la réalité est-elle concevable », « peut-on concevoir l’inconcevable » (peut-on nommer l’innommable). Ça me semble un peu une tentative de formalisation du problème de la recherche scientifique. (est-ce qu’on peut trouver ce qu’on cherche pas?) Est-ce qu’on peux spécifier la totalité de la réalité ?

Du coup, on peut se demander si ce n’est pas voué à l’échec. Toute formulation de ce problème est voué à s’enfermer dans son propre cadre théorique. D’une part, effectivement il est trivial qu’on a accès qu’à l’univers observable en l’état des connaissances actuelles. D’autre part, cette formalisation elle même, si on prend la réciproque de ta propre affirmation que tout ce qui est entendable ou logique peut s’exprimer en langage naturel, peut s’exprimer dans une logique.

Et là, on tombe sur des considérations Godelienne :) dans quelle mesure peut-on affirmer que l’axiomatique induite par cette formalisation est cohérente, ou indépassable ? Si elle est cohérente, elle est incomplète, et donc dépassable ? Ça ne contredirait pas un peu la transcendance de cette vision des choses ?

Tu prends là une condition suffisante (l'existence propre de l'objet expliquerait l'accord des observateurs), pour une condition nécessaire (leur accord ne peut s'expliquer que par une existence propre de l'objet, abstraction faite du rapport à l'observateur)

Il n’y a pas grand chose de ni nécessaire, ni suffisant dans l’accord entre observateurs pour montrer grand chose. L’observation est faillible par essence, et deux observateurs peuvent faillir de la même manière. On ne peux que constater que la méthode scientifique finit par générer quelque chose qui ressemble à un accord. Ce qui en soit est considéré comme une quasi religion pour Eintein ;) Et ce en tentant aux maximum de s’affranchir de nos biais et illusions en multipliant les méthodes d’observation. Cela dit si tu ne postules pas ça, il ne peux y avoir de sciences.

parler d'observation sans observateur (c'est-à-dire en faisant abstraction du rapport entre l'observateur et l'objet observé) est une contradiction dans les termes.

Je comprends pas trop en quoi tu postules que je veux me débarrasser de l’observateur. Il me semble assez naturel aussi de postuler que nos théories ne sont pas la réalité. A partir de là on peut déduire que l’homme, en tant qu’être doué de raison, tente juste de déceler l’ordre dans le monde en vue de le prévoir. Il réussit, ou il échoue ;)

Premièrement, l'accord entre observateurs sur les determinations spatio-temporelles des objets est tout sauf commun : voir les principes fondamentaux des relativité restreinte et générale.
L’accord entre observateurs existe aussi en relativité générale, je trouve ça assez moyen comme contre exemple. Il est simplement plus compliqué à établir, car il faut utiliser les équations de changements de référentiels prévus par la théorie. Il passe par ce proxy pour éviter ce qui pourrait sembler absurde à l’observateur humain naïf plongé prêt d’un trou noir ou en voyage spatial.

dans la connaissance expérimentale on ne pose jamais de questions sur ce que sont les choses en elles-même, mais seulement sur les résultats de nos observations;

Bien sur que si, il est impossible de concevoir une expérience scientifique un tant soit peu élaborée sans se poser des questions sur la nature de l’objet observé. Il est par exemple impossible de mesurer un quelconque spin d’une particule sans avoir postulé qu’il devait exister une telle quantité, ou qu’elle représentai quelque chose. Alors évidemment ça ne veut pas dire qu’on a une réponse absolue sur la nature de la chose qu,on veut observer, mais on a au moins l’idée (ou l_’espoir) que faire une telle expérience a un sens. Nos théorie ont pour vocation de nous renseigner sur la nature des choses. Ça implique nécessairement la question de la théorisation, qui est une étape loin d’être triviale à partir des observations. La relativité générale permet de restaurer l’accord

Je vois alors l'énoncé comme une fonction qui prend en entrée un interface{} et qui fait du typage dynamique : une assertion de type ou un switch (comme tu veux), comme en Go.

Je comprend bien l’idée, mais l’analogie trouve ses limites vu que la logique du premier ordre n’est pas constructive. Si x n’appartient pas à Oméga, ben, rien, ça ne pose pas de problème. Donc « exécution » n’a pas trop de sens. Par contraste, en python, si tu passes un objet d’un mauvais type à une fonction, ben « boom ». Python se comportera pas bien du tout … Alors que dans une implication logique, un ensemble qui ne vérifie pas la prémisse ne sera jamais susceptible de fournir un contre exemple de l’implication.

La notion de type capture bien mieux que celle d'ensembles (au sens de ZF) la notion logique de concept.
Je te suis pas. C’est une notion logique la notion de concept ?

ce ne sont que de simples phénomènes qui n'ont pas d'existence propre en dehors de leur rapport à un observateur.

Le truc qui me choque à chaque fois que je croise ce genre de philosophie : et quand il y a 2 observateurs ? Et que par hasard ils sont d’accord, ce qui n’est pas systématique, mais assez commun. On peut donc arguer qu’ils tirent les mêmes conclusions sur l’objet en question, ce qui tend à montrer que ces phénomènes ont une existence propre. On ne cherche pas autre chose que nous rassurer sur la pertinence de nos observations en sciences en tentant de rendre les résultats reproductibles.

ZF c'est l'archétype du typage dynamique
Je suis intéressé par une explication là dessus. ZF est bien fondée dans le sens ou toute compréhension est associée à un ensemble préexistant https://fr.wikipedia.org/wiki/Sch%C3%A9ma_d%27axiomes_de_compr%C3%A9hension « Étant donné un ensemble A et une propriété P exprimée dans le langage de la théorie des ensembles, il affirme l'existence de l'ensemble B des éléments de A vérifiant la propriété P. » ce que j’interprète (librement) comme une relation de sous typage. Étant donné que le « x ∈ A » ressemble quand même pas mal à une assertion de type et qu’elle est nécessaire dans une théorie des ensemble, j’ai du mal à comprendre en quel sens ça correspond à un langage dynamique.

Ce que Kant a prouvé, par exemple, dans la Critique de la Raison Pure c'est que le concept de cause (qui sert à expliquer les changements d'états des choses réelles dans le monde physique) n'est pas un concept d'origine empirique, mais un concept que nous imposons nous même à la nature en vertu de la structure formelle de notre esprit

Mouais, je t’aurai suivi si tu avis dis que c’est une structure que nous suivons dans la manière dont nous représentons la nature (à la rigueur on peut modéliser les réseaux de neurones qui permettent d’anticiper les mouvements d’un projectile) mais quant-à plier la nature à la manière dont nous la représentons j’ai plus de doutes ;) Après effectivement on peut arguer que le cerveau fait des calculs de probabilité conditionnelles - http://www.college-de-france.fr/site/stanislas-dehaene/course-2012-02-21-09h30.htm très intéressant au passage - de là a dire que l’invention du concept de causalité est subordonnée à ça, ou si nous étions condamnés à l’inventer … Si notre propre observation de notre connaissance intuitive du mouvement (façon métacognition) nous prédestinait à inventer la causalité et à décrire le monde de cette façon, c’est possible par contre. Du coup c’est plutôt par l’émergence de système de survie efficace capable d’anticiper qu’il nous est apparu …

Enfin il faut faire attention à lier (si A alors B) avec un raisonnement causal, tu prends le risque de lier corrélation et causalité. « Si A alors B » en logique, c’est à chaque fois que A, on a B aussi. Pas « A cause B ». Tu parles sans doute des logiques constructives, spécifiquement, qui s’interprètent différemment ( https://en.wikipedia.org/wiki/Constructive_proof )

Ce que je voulais dire par « enrichis » c’est que Kant n’a jamais défini un de ces système formels. Par conséquences les jugements qui y sont afférents lui étaient inaccessibles. Tu peux arguer qu’il est possible de faire la même chose en langage naturel, mais il faut le contraindre de manière à ne garder que les jugements valides dans le système de règle défini. Or il n’a jamais décrit ces contraintes (enfin je te laisse l’infirmer ;).

Sinon d’accord, j’aurai probablement du dire, la cohérence dans l’axiomatique du modèle sous-jacent. Que l’on peut considérer comme vraie d«s lorsque qu’il en existe un modèle (au sens de la théorie des modèle) qui tient mathématiquement la route. Ce qui ne devrait pas être bien sorcier pour une théorie des types ou pour une logique du premier ordre.

Sinon il semble que la définition de la cohérence comme absence de contradiction soit aussi communément admise. https://fr.wikipedia.org/wiki/Coh%C3%A9rence_(logique)

Il y a quand même une légère différence dans les détails :) J’ai l’impression que tu décris une sorte de « principe de réflexion » de la pensée abstraite dans la logique formelle, comme dans l’univers constructible de Gôdel ( http://www.madore.org/~david/weblog/d.2013-03-19.2124.constructible.html ) ou les ensembles et leur structure décrit par un rang inférieur se reflètent dans les rangs supérieurs de différentes manières.

Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)

Ne le prend pas mal, mais c’est de la naïveté. N’importe quel ingénieur sait qu’un composant a un domaine de validité et ne fonctionnera pas correctement en dehors. En informatique on a juste tendance à faire comme-ci on avait des vrais machine de Turing avec des bandes de mémoire illimitées. Ce n’est évidemment jamais le cas.

C’est juste que les données sont en général tellement petites qu’on peut faire « comme si » pour des kilos d’applications. Après dés que tu commences à jouer avec des algos exponentiels sur des problèmes NP-complets, tu comprends que c’est une fiction …

Ici, dans la recherche en langage de programmation, ils cherchent à encoder pas mal de choses dans les types. Ils ne seraient pas fâchés que par exemple on puisse coder ces règles métier dans les types, je pense. C’est un peu différent dans l’approche mais la méthode B permet d’en spécifier formellement dans l’invariant. 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. Genre que la sortie d’une fonction qui a la propriété de trier c’est que chaque élément est inférieur au suivant. Ç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.

Si tu écris du code qui respectent pas ces règles encodées, l’objectif c’est que ça ne compile pas. Si tu écris deux règles qui sont incompatible l’une avec l’autre, logiquement, l’objectif est que ça te dise « t’es bien mignon mais c’est impossible de maintenir la propriété que la somme des surface est la somme de l’immeuble si tu modifie pas la taille de l’immeuble quand tu modifie la taille d’un appart » et que ça compile pas, itou. 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.

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.

Donc tu as un cas d’utilisation avec des arbres profonds pas profonds ? cqfd.

Tu es dnc ptete sur le cul mais t’es en plus à côté de la plaque ;) Moi ça me choque pas qu’un programme te dise honnêtement « je suis pas conçu pour ce genre de cas » et s’arrête. Ce qui me choquerait c’est que ça segfaulte salement. D’une manière générale, c’est pas une mauvaise pratique de fixer des limites.

Ben non justement, vérifier la cohérence interne veut dire que tu vérifie sans faire référence au monde extérieur que tes spécifications se tiennent elles mêmes et ne sont pas contradictoire en soi. Puis que ton programme est bien cohérent avec les spécifications.

Imagine que différents secteurs de l’entreprise aient différentes représentation d’un même produit. Elles n’ont pas la même vision, le service design, le service compta et le service marketing n’ont pas besoin des mèmes informations. Le SI peut par contre vérifier qu’il y a une certaine cohérence entre ces représentation.

En terme de cohérence, un ami m’a par exemple parlé d’un client promoteur en indiquant que le client voulait pas vraiment être sur que la surface disponible dans un immeuble était égale à la somme des surface des appartements. Dans le cas d’un client honnête, si il recherche à maintenir cette propriété, il est possible de vérifier que le programme garantit qu’un employé ne va pas aller tricher avec les données en bidouillant n’importe comment.

Le « modèle métier » c’est plutôt le modèle qui va te dire qu’un avion a en général deux ailes chez Airbus, ou que le débit et le crédit d’un compte bancaire doivent s’équilibrer chez un comptable.

Et c’est indépendant de la correction du compilateur, vu que c’est la cohérence «interne». La correction du compilateur garantit que ces propriétés seront préservées par la compilation.

Moué, ça se voit la que tu racontes n’imp.

La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. Mais effectivement elle va pas créer ex nihilo le modèle métier ou une théorie scientifique. Ça mettrai un paquet d’universitaires et d’informaticiens au chomage :) Mais du point de vue de la cohérence, ça peut lever des lièvres.

D’une manière générale, dire « aucune limite » c’est un raccourcis pour dire « toute la mémoire dispo ». En vrai, ça finira toujours par planter pour certains niveau d’imbrications - si c’est pas la pile qui explose, ce sera le tas. Si c’est pas le tas, ça sera le dd si t’as été pervers au point d’utiliser un fichier pour compter les accolades. Ça donne un fichier suffisamment grand pour toutes les applications réalistes, mais qui existe tout de même.

Et puis si t’en es à devoir traiter un arbre très très profond - alors que tout le point d’un arbre c’est en général de maintenir un certain niveau d’horizontalité et d’éviter de partir en profondeur (un index typiquement, que tu essayes de maintenir équilibré) t’as probablement d’autres préoccupations. Un arbres très profond, si on le suppose équilibré, ça veut dire que la taille des donnée est exponentiellement plus grande, donc absolument gigantesque. Peu de chances que ça termine dans un fichier json, en somme.

Un soucis de maturité des comportements sur LinuxFR ?

Et une culture chez certains contributeurs vis à vis de la sécurité je pense. Avec une idée « le seul moyen de corriger une faille c’est de l’exploiter » qui incite a des comportements complètement non naturels genre des comptes problématiques qui apparaissent opportunément pour troller. Ça incite à des postures excessivement défensives. Genre par crainte de de comportement détester jouer une caricature à la puissance 10 dudit comportement afin de pousser à l’interdire.

J’ajouterai perso que la théorie sur la sémantique d’un langage, ça devrait largement aider à construire un outillage puissant pour l’écosystème du langage.

L’exemple de l’inférence de type est un cas d’école, je pense : c’est une fonctionnalité très bien comprise théoriquement, qui permet d’aider le programmeur à faire moins d’erreur. La coloration syntaxique, c’est quand même utile d’avoir une grammaire formelle pour l’implémenter, et ces objets sont très bien connus théoriquement. Ça fait partie du baggage de base d’un informaticien. Peut être d’ailleurs qu’un des boulot du chercheur en langage c’est d’essayer de penser à des outils que la formalisation des langages peut aider à concevoir … après tout si c’est plus régulier et plus compréhensible pour les humains, c’est aussi très utile pour les machines pour raisonner sur le programme …

Ah oui pardon, j’ai dû être trompé par « Dans cette partie du texte, quand je parle de "voir un programme comme un objet mathématique", je parle plutôt du code source ». Toujours cette satanée confusion … c’est absolument pas naturel pour moi de considérer le code simplement comme un programme.

On est pas aidé par des expressions comme langage formel. En fait un langage de programmation (ou sa formalisation) est du côté des système formels, un langage formel en fait simplement partie. Le système formel est constitué du couple (langage formel, sémantique), et on est d’accord que la grammaire définit la partie « langage formel ».

Alors la façon dont je définis "un programme" c'est en donnant, par exemple, une syntaxe BNF qui, on est d'accord, correspond bien au choix d'un certain langage de programmation. Mais ce n'est pas à ce moment qu'on définit le langage, c'est seulement ensuite, une fois qu'on a défini ses programmes.

Ça se discute. Tu notes une relation de temporalité (voire de causalité) qui n’existe pas forcément dans le monde mathématiques. On ne définit pas les entiers en donnant tous les exemples d’entiers, et une fois qu’on l’a fait, on définit les entiers. On donne des axiomes qui permettent de décider si un objet du formalisme est ou pas un entier. Par l’axiome d’extensionnalité, à tout prédicat correspond une extension : « Étant donné un ensemble A et une propriété P exprimée dans le langage de la théorie des ensembles, il affirme l'existence de l'ensemble B des éléments de A vérifiant la propriété P » https://fr.wikipedia.org/wiki/Sch%C3%A9ma_d%27axiomes_de_compr%C3%A9hension . Mais à chaque propriété sur un ensemble correspond une seule extension … que tu définis « en même temps » que tu donnes la propriété. En complexité, on définit même un problème de décision comme l’appartenance ou pas d’une chaîne à un ensemble. Le prédicat associé à l’ensemble n’est même pas évoqué … En gros dans mon esprit la BNF (le prédicat) définit l’ensemble (le langage). Sauf si tu assimiles l’écriture de la BNF à la définition d’«un» programme, mais c’est pas du tout ma vision des choses. Enfin cette manière de décrire les choses correspond peut être à une vision constructiviste des choses ;).

Sinon je suis entièrement d’accord pour ce que tu dis sur la formalisation, avoir un accord parfait entre la théorie et l’expérience est un acte inaccessible. Cela dit, je pense avoir identifié un truc qui manque dans ton texte : il est considéré comme implicite que le programme est destiné à être exécuté. Du coup la métaphore du « parler » tombe un peu à plat. Quand je fais une requête google, je « parle » à la machine, pourtant je ne la programme pas. Un programme est destiné à être exécuté, et peut être exécuté pleins de fois. ça ne transparaît dans ton texte que quand tu parles de comportement du programme. Ce qui pourrait lever ton ambiguïté d’ailleurs.

(et je poste en l’état parce que j’y ai déjà passé trop de temps)

Je dirai que « les informaticiens ont inventé de nombreuses manières de décrire les programmes qui sont exécutés par un ordinateur » conviendrai dans un premier temps. Tu peux rajouter « souvent ils sont écris sous forme de texte, parfois d’autres formes, ou d’autres formes symboliques (« graphiques » par ex. https://scratch.mit.edu/) ». Dans tous les cas, le formalisme qui permet de les décrire constitue ce qu’on appelle un « langage de programmation ». »

L'idée c'est qu'on peut représenter un programme (dans un langage donné) comme un objet mathématique, et à partir de cela définir le langage.

Je comprend pas. Un programme écrit dans un langage donné est quelque part déjà un objet mathématique. « et à partir de cela définir le langage » euh, on commence pas par définir le langage avant d’écrire des programmes ??? Peut être qu’il faut que tu parles de sémantique (en général) d’un langage de programmation, sinon pareil je pense que ça peut ne pas être clair pour un débutant.
Je propose :

«Les informaticiens apprennent souvent par l’exemple et la pratique (et un prof et ses explications) ce qu’est supposé faire un programme et se forgent une intuition de la signification du code qu’ils écrivent, Ensuite, on essaye de le faire tourner pour voir si « ça marche » … et parfois, « ça marche ».

Les approches formelles s’appuient sur autre choses que l’essai et l’erreur et s’appuient sur la logique et les mathématiques pour décrire le comportement attendu d’un programme (indépendamment de ce qui se passe vraiment quand on le teste). La sémantique formelle (cette fois) d’un langage permet de faire le lien entre chaque programme écrit dans ce langage et ce comportement attendu. Votre boulot est en partie de l’écrire et de l’imaginer.»

Du coup vous vous nourrissez de la rigueur des maths pour détecter d’éventuels problèmes, et le point de vue différent offert peut donner de nouvelles idées et définir des choses précises là ou les langages de programmation « défini par l’implémentation ou la doc » sont moins précis et solides, peuvent avoir des trous et des points non documentés ou on est vraiment obligé de tester pour savoir ce que ça fait « en vrai ». Non ?

Intuitivement on pense à le définir comme un ensemble de programmes, mais en fait il faut aussi donner leur sémantique, c'est-à-dire donner le lien entre le programme (le texte) et le comportement quand on le lance (aussi représenté comme un objet mathématique.

« Intuitivement on pense à le définir comme un ensemble de programmes » Mmm certainement pas l’intuition d’un débutant … En fait ce que tu entend par « programme » n’est pas forcément clair. Et cette intuition de programme en tant que composition de programme interroge sur une notion de « programme primitif » qui est un peu HS et pas du tout intuitive pour quelqu’un qui ne connait pas la programmation. C’est un peu une impasse, je pense.

J’imagine que par « mathématiquement » tu veux dire « dans un formalisme logique ».

Attention, on peut aussi représenter mathématiquement un algorithme, mais l'objet mathématique qui correspond à un programme C par exemple n'est pas le même que celui qui correspond à l'algorithme implémenté

Il faut que tu utilises soit un langage algorithmique basique, qu’on peu facilement assimiler à un langage de programmation, soit des formules déclaratives (dans une logique) pour décrire des propriétés du résultats. La preuve visera à démontrer que les opérations décrites par l’algo réalisent bien les propriétés attendues. Ton utilisation de « mathématique » me gène en fait, en tant que personne qui connait un peu le domaine.

Autre remarque :

La sémantique d'un langage est alors donnée par une relation (mathématique) entre les programmes et leur comportement.

Je pense que c’est clair uniquement pour ceux qui savent ce qu’est une relation mathématique.

Ça n’absorbe pas grand chose si le papier finit cramé. Le CO2 est relargué relativement rapidement. Au mieux le bilan carbone de la filière est neutre si ces bois produisent suffisamment de matière pour l’industrie du papier, et en ignorant les énergies nécessaires au transport et à la fabrication du papier.

En plus pour des bouquins qui seront lus souvent une fois ou resteront invendus et termineront direct au pilon et au recyclage … voire prendront de la place et de la poussière dans une bibliothèque.

Cela dit j’aime bien le support papier, mais c’est pas ces forets d’exploitation qui vont le sauver. Le bilan d’une liseuse est probablement désastreux aussi, mais c’est sans doute mieux pour la forêt et la biodiversité en général. Petite pensée opur tous les auteurs qui ne sont pas Amélie Nothomb et qui peinent à se faire éditer aussi.

Je trouve ça dans l’ensemble très clair et très intéressant, même en étant pas la cible. Après je pense que la première phrase est un peu sèche pour un béotien (« représentation symbolique », ça peut faire peur, ce serait dommage). Et tu ne reparles pas de symbole dans la suite, donc l’utilité est sans doute discutable.

Quelques remarques :

Je pense aussi que tu peux intervertir « formalisation mathématique d'un langage de programmation » et « sémantique formelle ». Le second est plus technique, utiliser la première expression en définissant la seconde.

on lui donne une sémantique formelle (ou plusieurs) en définissant les programmes comme des objets mathématiques

Un peu ambigu je trouve, mais c’est pas très grave, et peut être un peu confusant : le programme peut être considéré comme la spécification d’un algorithme dans un langage, alors que la sémantique formelle peut être considérée comme la spec du langage lui même. Ou alors tu veux dire que si le langage n’a pas de sémantique formelle, on ne peut pas considérer le programme comme un objet mathématique ? Mais je pinaille peut être un peu beaucoup pour ce que tu cherches à faire.

Tu entends quoi par "de plus en plus buggué" ? C'est étrange car encore maintenu.

J'espère que vous allez mettre débattons sur les rails, et pas dans les roues !

Alors que je suis juste tombé sur un nid de gens contre le progrès sur Internet blasés !