Lazi

Essai 2

On a parfois envie d'arrêter de courrir tête baisser et prendre un moment pour faire le point. Nous allons dans le domaine des langages informatiques et cela nous permetra de présenter les innovations de grande ampleur amenées par le nouveau langage de programmation Lazi.

Les révolutions scientifiques viennent souvent de remises en questions d'idées admises. Par exemple Einstein a remis en question la notion de simultanité pour la théorie de la relativité. Nous allons remettre en questions quelques idées reçues puis plus loin voir comment faire autrement (mieux). Nous verrons au final que cela nous mène à un langage plus esthétique, plus simple et pourtant plus puissant que ceux actuels.

Des idées acceptées

Les fonctions informatiques et mathématiques sont différentes.

Nous savons déjà que les langages fonctionnels pures (comme l'excellent Haskell) ont remis en question cette idée et à quel point cela est un progrès. Mais cette solution n'est que partielle dans le sens où les fonctions informatiques qui contiennent des entrées sorties ne sont pas vues comme des fonctions (mais des monades en Haskell). Nous allons voir qu'il est possible d'aller plus loin et de voir toute fonction informatique comme une fonction mathématique (même print).

Il est normal de limiter l'expression des contraintes à vérifier.

Une fonction des types habituelle est de vérifier des contraintes sur le code source. On peut par exemple exprimer la contrainte qu'une fonction prend en argument un entier et retourne un réel, mais souvent ne peut pas exprimer que la fonction ne boucle pas, car l'expression des contraintes est limitée.

Il est normal que le compilateur pose des contraintes sur le fichier(l'exécutable ou la librairie) produit.

Actuellement un compilateur ne peut pas par exemple produire plusieurs librairies en une fois ou encore un programme et des fichiers de données ou encore un programmes comprenant des nouvelles optimisations non prévues à la base. Nous verrons qu'il est possible de pouvoir produire absolument tous le/les fichiers que l'on souhaite.

Un compilateur doit assez rapidement :

  • déterminer la validité du source
  • produire un éxécutable
Cette idée adminise est gênante car elle limite l'expressivité d'un code source car la complexité d'un programme est illimité et imposer de telles contraintes au compilateur limite les possibilités du langage.

Il est normal qu'un langage pose des limites dans la structure du code source :

  • il n'est pas possible d'utiliser différents languages dans une même source (par exemple un code source comprenant du javascript et du C++ qui soit tous les deux compilés en un même programme.
  • Il n'est pas possible de définir et d'utiliser de nouvelles structures de contrôle de haut niveau, c'est pourquoi le complilateur est souvent modifié pour intégrer des innovations.
  • Il n'est pas possible de manipuler des entités du langages de haut niveau, par exemple une fonction ne peut pas retourner un type (mais juste une rvalue d'un certain type).

Nous verrons que ces limitations peuvent ne sont pas intrisèques à l'informatique.

Éliminer simplement ces limitations

Nous allons rapidement expliquer comment ces limitations sont dépassées. Chacunnes des innovations sont détaillées dans d'autres articles. Nous allons commencer par la plus paradoxale :

Les fonctions informatiques sont des fonctions mathématiques

Il reste à traiter des fonctions avec effet de bord. La solution utilisée par Lazi existe déjà dans la vie de tous les jours par l'idée suivante "et si tout ce qui m'est extérieur n'existait pas vraiement et soit une production de mon esprit ?". Par cette idée vous vous placez au centre de toute chose. En l'appliquant à l'informatique cela consiste à définir une valeur U qui représente l'univers extérieur à la fonction. U comprend tout ce qui est entrée/sortie du point de vue de la fonction (stdin, stdout, la mémoire globale etc). Par exemple la fonction print "hello world" se traduit par print U "hello world" et cette fonction retourne le nouvel univers qui aura subit la modification d'envoyer "hello world" dans stdout. Bien sûr on créera une syntaxe pour rendre son utilisation aisée. Pour voir les détails techniques et les avantages, lire l'article traitant du sujet plus en détail.

L'expression sans limitation des contraintes à vérifier

Pour cela nous utilisons le langage mathématique à la base de Lazi, plus la possibilité d'aider la fonction de preuve quand les aides automatiques aux preuves n'y arrive pas.

Un compilateur sans contrainte sur le/les fichiers produits

Pour cela nous passons à un niveau d'abstraction supplémentaire : le code source ne représente pas le programme à produire mais est une fonction qui retourne la représentation de fichiers. Cette technique déporte la compilation dans le code source même qui utilisera différentes librairies. Cela n'est possible qu'avec un langage entièrement mathématique permetant d'exprimer des contraintes de haut niveau. Voir l'article sur le sujet.

Un code source sans limite

En Lazi le code source est une fonction mathématique, la mathématique lazi est intégrée au langage, on peut l'utiliser pour formuler des preuves, définir des extensions mathématiques et définir des nouveaux langages informatiques tout en fournissant les preuves de leurs validités. Cela parait abstrait et de haut niveau, mais cela permet à la fois :
  • au développeur de base javascript d'utiliser Lazi pour produire un programme (il n'aura qu'à rajouter quelques lignes au début pour sépcifier qu'il écrit son programme en javascript)
  • au développeur de plus haut niveau de, par exemple, ajouter des types à javascript pour exprimer de nouvelles contraintes (par exemple sur le temps d'éxécution) qui permetrons au développeur javascript de s'assurer que le source respecte des contraintes de temps réel.
Ce "sans limite" est vraiement très large. Par exemple un inconnu peut fournir au monde entier une nouvelle manière de compiler qui accélère les exécutables sans passer par un comité de vérification et sans causer de bug car il aura fourni la preuve de validité de son extension. Ce qui ferai que du jour au landemain votre compilateur deviendrait plus efficace sans avoir strictement rien à faire car les preuves mathématiques fournissent la certitude d'une conformité parfaite.