Disjonction de cas, ou recherche d'exhaustivité, dans les quelques sous-cas ou par l'énumération d'une grande combinatoire par la machine à calculer.
Correspondance de Curry Howard : si on définit les ensembles de départ et d'arrivée, cela fournit-il suffisamment de contraintes pour induire l'implémentation de la fonction. aka équations fonctionnelles en mathématiques (relation log, exp, équations différentielles).
Définir une fonction par des propriétés (contrat d'interface, tests unitaires) implique l'expression de la fonction de fil en aiguille.
A contrario, une équation fonctionnelle peut ne pas avoir de solutions.
Concept de refactorisation de code, l'idée qu'on peut obtenir de nouvelles propriétés intéressantes en simplifiant les expressions, les termes ou le code s'annulant par lui-même et exposant sa propre nature !
Un système de contraintes peut être vue comme une liste de propriétés liées. En programmation fonctionnelle, on peut supposer des propriétés temporairement vraies à la manière de conjectures et établir une série de relations constituant un système. Le tout devenant cohérent fournit une sorte de preuve et signifie que le programme fonctionnera concrètement !
Ou bien au contraire les absurdités peuvent arriver, et on aboutit à une théorie bancale et fausse !
Cette dualité entre les types et le système de règles implicites associées justifie la technique dite d'analyse dimensionnelle (thm de Curry-Howard).
La puissance de la notation
Classiquement le nombre d'opérateurs dans un langage de programmation orienté objet est restreint. Les classes permettent d'associer des méthodes à des objets mais de manière verbeuse.
En quelques caractères, on peut inventer un concept et le manipuler de manière pratique avec des symboles typographiques.
e^iPi + 1 = 0, les équations de Maxwell, de Newton etc. cachent des concepts riches vecteurs, nombres complexes, géométrie etc.
Moralité de l'histoire
Il faut réintroduire de la rigueur dans le raisonnement de la programmation.
La méthode startup ship it fix it later n'est pas la bonne.
Les autres disciplines d'ingénierie mécanique, électrique, chimique basent leur raisonnement sur une théorie mathématique, il n'y a pas de raison que ça n'en soit pas de même pour l'ingénierie logicielle.
Tout comme dans les autres sciences les professionnels réintroduisent progressivement de la rigueur après avoir développé des idées pratique.
Collections = Ensembles
Pas de boucles, ni même de boucles imbriquées
Chaining of effects, utilisation de la notation avec de multiples indices
Disjonction de cas, ou recherche d'exhaustivité, dans les quelques sous-cas ou par l'énumération d'une grande combinatoire par la machine à calculer.
Correspondance de Curry Howard : si on définit les ensembles de départ et d'arrivée, cela fournit-il suffisamment de contraintes pour induire l'implémentation de la fonction. aka équations fonctionnelles en mathématiques (relation log, exp, équations différentielles).
Définir une fonction par des propriétés (contrat d'interface, tests unitaires) implique l'expression de la fonction de fil en aiguille.
A contrario, une équation fonctionnelle peut ne pas avoir de solutions.
Concept de refactorisation de code, l'idée qu'on peut obtenir de nouvelles propriétés intéressantes en simplifiant les expressions, les termes ou le code s'annulant par lui-même et exposant sa propre nature !
Un système de contraintes peut être vue comme une liste de propriétés liées. En programmation fonctionnelle, on peut supposer des propriétés temporairement vraies à la manière de conjectures et établir une série de relations constituant un système. Le tout devenant cohérent fournit une sorte de preuve et signifie que le programme fonctionnera concrètement !
Ou bien au contraire les absurdités peuvent arriver, et on aboutit à une théorie bancale et fausse !
Cette dualité entre les types et le système de règles implicites associées justifie la technique dite d'analyse dimensionnelle (thm de Curry-Howard).
La puissance de la notation
Classiquement le nombre d'opérateurs dans un langage de programmation orienté objet est restreint. Les classes permettent d'associer des méthodes à des objets mais de manière verbeuse.
En quelques caractères, on peut inventer un concept et le manipuler de manière pratique avec des symboles typographiques. e^iPi + 1 = 0, les équations de Maxwell, de Newton etc. cachent des concepts riches vecteurs, nombres complexes, géométrie etc.
Moralité de l'histoire
Il faut réintroduire de la rigueur dans le raisonnement de la programmation. La méthode startup ship it fix it later n'est pas la bonne.
Les autres disciplines d'ingénierie mécanique, électrique, chimique basent leur raisonnement sur une théorie mathématique, il n'y a pas de raison que ça n'en soit pas de même pour l'ingénierie logicielle.
Tout comme dans les autres sciences les professionnels réintroduisent progressivement de la rigueur après avoir développé des idées pratique.