Stage au sein de l'équipe JSCert — Été 2015 — Rennes
Présentation de l'équipe JSCert
JSCert est un projet de recherche commum entre l'INRIA de Rennes et l'Imperial Collège de Londres qui a pour objectif de fournir une formalisation en Coq du standard JavaScript (ECMAScript 5) écrit en anglais.
Le langage JavaScript est un des langages phares, sans qui le web ne serait pas ce que l'on connait aujourd'hui. Le standard de JavaScript est écrit de façon a ce qu'il n'y ait pas de comportements indéfinis (ce qui est par exemple l'exact opposé du standard du langage C).
Cependant, sa spécification ne donne pas de sémantique formelle et les différentes implémentations de JavaScript (entre autres V8 de Google, Chakra de Microsoft, SpiderMonkey de Mozilla) vérifient qu'ils respectent le standard en vérifiant que leurs implémentations sont conformes à la suite de tests 262.
Un effet de bord de cette volonté est qu'un programme JavaScript ne plante jamais vraiment ; plutôt que de planter il aura un comportement qui n'est pas forcément celui que le développeur aurait voulu.
L'équipe JSCert propose une référence éxécutable de JavaScript (JSCert) et un interpréteur certifié correct (JSRef) vis à vis de JSCert. Cette référence exécutable de JavaScript peut être utile aux développeurs JavaScript qui veulent débogguer leurs applications ou encore aux développeurs des moteurs JavaScript pour vérifier que leur implémentation est conforme au standard.
Contexte du stage
Pouvoir dégogguer du JavaScript avec un interpréteur Coq est certes intéressant, cependant, il ne faut pas s'attendre à ce que les développeurs JavaScript utilisent un déboggueur écrit en Coq.
L'objectif de ce stage fut de développer les débuts d'un backend JavaScript au compilateur d'OCaml et de produire un code instrumentable pour au final avoir un déboggeur JavaScript en JavaScript (le code OCaml certifié produit par Coq pouvant être alors transformé en JavaScript).