Re: essayer Julia ?

Je vais me faire l'avocat du diable mais allons y...

Objection rejetée ! :-P

Non que je sois en désaccord avec ce que tu dis, mais tu as mal interprété mes propos (peut être bien par ma faute, je me suis sans doute mal exprimé). Je n'ai jamais dit cela :

Réduire l'informatique aux Maths et à la preuve formelle uniquement est une stupidité.

autrement elles ne seraient pas traitée comme deux sciences distinctes, mais la première serait simplement une branche de la seconde. Néanmoins quand je regarde l'image de ton message, la première impression qui me vient à l'esprit est celle-ci : elle a été faite par un ingénieur, autrement dit une personne qui se fait une fausse idée de ce qu'est la science mais qui veut tout de même exprimer son avis dessus.

Il n'en reste pas moins que les mathématiques et la preuve formelle fournissent les outils conceptuels, par exemple, pour les systèmes de typage langage de programmation. Je reprends mon exemple de Pythagore : si en entrée tui lui donnes un carré, il va te répondre qu'elle n'a pas le bon type, lui il veut un triangle rectangle ! Par contre, tu as un autre théorème qui te dis que si tu coupes un carré selon sa diagonale, tu obtiens deux triangles rectangles. Et boum, en composant les deux théorèmes, tu résous le problème de la duplication du carré : à partir d'un carré donné, construire un carré de surface double. La démarche est strictement similaire, dans l'organisation du discours, à ce que l'on fait en programmation en découpant le code en fonctions que l'on combine ensemble. D'un problème compliqué, on le découpe en problème plus simple, et on obtient la solution par composition : divide and conquer. On obtient alors ce parallèle entre informatique et mathématique :

Informatique	Mathématiques
Type	Formule
Programme	Preuve
Primitive système	Axiome
Fonction de A vers B	Preuve de « A implique B »
Paire de A et B	Preuve de « A et B »
Type somme sur A et B	Preuve de « A ou B »
Interpréteur	Théorème de correction
Décompilateur	Théorème de complétude

J'ai repris le tableau de la dépêche de Perthmâd sur Coq 8.5, tu pourras t'y reporter pour de plus amples développements.

Je régissais au départ à cette proposition d'arnaudus :

Le lien entre les maths et la programmation est ténu, en plus d'être souvent dangereux. L'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout.

Les liens sont tout sauf ténus, soutenir le contraire est une ineptie. Mais reprenons un exigence d'arnaudus :

(efficacité de l'algorithme en temps et en mémoire, gestion des arrondis, évolutivité, modularité et clarté du code)

La pensée mathématique ne serait-elle pas totalement modulaire, par exemple ? Le travail des algébristes, par exemple, qui classent leurs structures en monoïdes, groupes, groupes abéliens, anneaux, corps, espaces vectoriels... Et en algèbre linéaire, pour reprendre le calcul sur matrices, les théories parlent d'espaces vectoriels sur un corps quelconques (le corps des réels n'étant qu'un corps particuliers), les théorèmes et preuves sont faites sur un corps des scalaires quelconques : la voilà la programmation générique et la modularité ! On voit la route s'ouvrir vers le polymorphisme paramétrique, i.e. les types paramétrés, les templates du C++, les generics du Java et j'en passe (voir le besoin exprimé par l'échange entre Gabbro et Albert_ plus bas dans le fil de discussion).

Illustration avec le concept le plus simple : le monoïde. C'est une structure munie d'une opération interne et d'un élément neutre pour celle-ci (comme les entiers avec l'addition).

module type Monoid = sig
 type t
 val e : t
 val op : t -> t -> t
end

À partir de là, on peut facilement, sur un monoïde donné, répéter l'application de l'opérateur interne sur une suite d'élément, comme lorsque l'on calcule la somme 1 + 2 + 3 + 4.

let sum (type a) (module M : Monoid with type t = a) =
 List.fold_left M.op M.e

Maintenant, outre les entiers munis de l'addition avec 0 pour élément neutre, on peut remarquer que les string muni de l'opération de concaténation forme un monoïde avec pour élément neutre la chaîne vide "".

module String_mon = struct
 type t = string
 let e = ""
 let op = ( ^ )
end

On peut faire pareil avec les int et l'addition, les int et la multiplication, ou bien encore les listes et l'opération de concaténation.

module Int_plus_mon = struct
 type t = int
 let e = 0
 let op = ( + )
end
module Int_mul_mon = struct
 type t = int
 let e = 1
 let op = ( * )
end
module List_mon (T : sig type t end) : Monoid with type t = T.t list = struct
 type t = T.t list
 let e = []
 let op = ( @ )
end

Voyons voir à l'usage :

sum (module Int_plus_mon) [1; 2; 3; 4];;
- : int = 10
sum (module Int_mul_mon) [1; 2; 3; 4];;
- : int = 24
sum (module String_mon) ["Hello"; " "; "World!"];;
- : string = "Hello World!"
sum (module List_mon(struct type t = int end)) [[1; 2]; [3; 4]];;
- : int list = [1; 2; 3; 4]

Et là je définis le produit scalaire comme en Python dans mon commentaire précédent, mais avec la garantie du typage statique (le type checker vérifie que ma preuve n'a pas de vice de forme) :

let dotprod v1 v2 = sum (module Int_plus_mon) (List.map2 ( * ) v1 v2);;
val dotprod : int list -> int list -> int = <fun>
dotprod [1; 2; 3] [3; 4; 5];;
- : int = 26

On peut aller plus loin, là c'était un simple échauffement. :-) L'exemple vient d'une bibliothèque dont l'annonce de publication a été faite hier sur le forum OCaml. Prenons un algorithme qui a cet forme :

algorithm a b ::=
 x := f a;
 y := f b;
 return (x + y);

où f est une fonction définie ailleurs dans le code. On pourrait aller plus loin puis le paramétrer par la fonction f et la fonction appliquée sur x et y avant d'être retournée.

 algorithm ((_ + _), (f _)) a b ::=
 x := f a;
 y := f b;
 return (x + y);

Ici le return et le point-virgule ; ont usuellement une sémantique bien définie par le langage : ce couple forme ce que l'on appelle une monade (là je sens les haskelleux venir en masse). On peut donc paramétrer l'algorithme par une monade et prendre de la liberté vis à vis d'une sémantique contrainte par le langage hôte :

algorithm ((return _), (_ := _ ; _)) ((_ + _), (f _)) a b ::=
 x := f a;
 y := f b;
 return (x + y);

le paramètre (_ := _ ; _), qui contrôle la sémantique du ;, est usuellement appelé bind. Ce qui donne la signature de module suivante :

module type Monad = sig
 type 'a t
 val return : 'a -> 'a t
 val bind : 'a t -> ('a -> 'b t) -> 'b t
end

et notre algorithme devient un module paramétré par une monade et un autre module qui contient les interprétations de + et f.

module Algorithm (M : Monad) (R : ... ) = struct
 open R
 open M
 let run a b =
 f a >>= fun x ->
 f b >>= fun y ->
 return (x + y)
end

ici >>= est un alias courant pour bind quand on joue avec les monades, et run sert comme son nom l'indique à exécuter le calcul. Il existe un paquet de monades intéressantes (en plus de celle avec le sens usuel de ; et return dans les langages impératifs), la documentation de la bibliothèque en question en donne quelques exemples (bibliothèque à la structure on ne peut plus modulaire). Et tout cela sert bien évidemment à produire des logiciels, en l'occurence le projet BAP (Binary Analysis Platform) :

The Binary Analysis Platform is a reverse engineering and program analysis platform that targets binaries, i.e., compiled programs without the source code. BAP supports multiple architectures (more than 30), though the first tier architectures are x86, x86-64, and ARM. BAP operates by disassembling and lifting the binary code into the RISC-like BAP Instruction Language (BIL). Thus the analysis, implemented in BAP, is architecture independent in a sense that it will work equally well for all the supported architectures. The platform comes with a set of tools, libraries, and plugins. The main purpose of BAP is to provide a toolkit for automated program analysis. BAP is written in OCaml and it is the preferred language to write analysis, we have bindings to C, Python and Rust.

Quand je regarde l'architecture de cette bibliothèque, la dernière pensée qui me vient à l'esprit est bien celle-ci : « l'idée d'adopter une pensée mathématique quand on code ne me semble pas une bonne idée du tout », mais au contraire je me dis : l'idée d'adopter une pensée mathématique quand on code me semble une excellente idée ! :-)

On veut un truc qui marche rapidement : on va au plus simple; on veut plus de sécurité : on adapte la monade; on veut travailler sur l'optimisation : on change le module de l'algorithme... Vous ne voyez toujours pas l'utilité ? Alors effectivement, toutes ces contraintes auxquels il faut s'adapter proviennent du monde extérieur et donc sont en quelques sortes extra-mathématiques, mais croire que la méthodologie mathématique est inadaptée, voire impropre, au besoin de l'ingénieur informaticien c'est ignorer ce que sont les mathématiques.

Et pour terminer sur ces histoires d'optimisation de code (et donc de compléxité algorithmique), je citerai la présentation du module Logique et théorie du calcul du MDFI :

La théorie de la calculabilité s'intéresse essentiellement à la question suivante : au moyen d'un ordinateur, quelles fonctions peut-on calculer et quels problèmes peut-on résoudre ? Son développement est concomitant de l'apparition des principaux modèles de calcul (fonctions récursives, machines de Turing, lambda-calcul,...) et est très étroitement lié à la logique mathématique : théorème d'incomplétude de Gödel (qui sera abordé dans ce cours), lambda-calcul typé (cours Preuves et types)...

La complexité cherche quant à elle à mesurer le degré de difficulté d'un problème, typiquement en termes de temps de calcul et d'espace utilisé. Il s'agit donc de questions plus fines, qui font l'objet de nombreuses recherches actuelles, notamment en rapport avec la logique.

L'objectif de ce cours est de présenter les outils et résultats fondamentaux pour aborder ces questions.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.