λ · remote 15: Coq, OCaml et Tezos et la recherche en langages de programmation

Alors que les événements "en vrai" reprennent, nous avons décidé de maintenir un format en ligne ! Et oui, ça nous donne de la flexibilité pour nos invités, pouvant venir de tout horizon, et grâce à cette flexibilité, vous accueillons deux invités exceptionnels pour notre 15ème édition !

= La recherche en langages de programmation
par Gabriel Scherer

Une partie des idées en programmation fonctionnelle sont issues du milieu de la recherche académique en langages de programmation. Mais comment travaille-t-on dans ce domaine, comment s'articulent la recherche et le développement d'outils, prototypes expérimentaux ou destinés à un plus large public ? J'essaierai de donner quelques réponses à ces questions, tirées de mon expérience personnelle de travail, au sein d'un milieu académique, sur le langage OCaml.

Gabriel Scherer est chercheur en langages de programmation à l'INRIA Saclay, et l'un des mainteneurs du langage OCaml. (http://gallium.inria.fr/~scherer/)

= coq-of-ocaml (présentation et usage dans Tezos)
par Guillaume Claret

Le traducteur `coq-of-ocaml` permet de transformer du code OCaml en un
code Coq similaire dans la mesure du possible. Coq étant un logiciel de
preuves, on peut alors faire de la vérification formelle de propriétés
valables sur notre code OCaml initial. Lorsque le code OCaml évolue, on
peut relancer `coq-of-ocaml` pour vérifier que les changements
n'introduisent pas de régressions pour les propriétés certifiées.
Nous présenterons le fonctionnement de l'outil sur le sous-ensemble
d'OCaml supporté (essentiellement le fragment pur ou monadique d'OCaml,
moins les fonctionnalités avancées comme les objets). Nous montrerons
aussi comment on se sert de `coq-of-ocaml` pour certifier des morceaux
de code critiques dans Tezos, une crypto-monnaie écrite en OCaml.

Guillaume Claret a fait sa thèse dans l'équipe qui développe l'assistant
de preuve Coq, et travaille depuis à faciliter l'utilisation de cet
outil de preuve formelle dans l'industrie. Il est actuellement
ingénieur-chercheur à Nomadic Labs, une entreprise de R&D sur la
blockchain Tezos, et lance la compagnie Foobar.land pour se dédier à la
preuve de programmes. (https://twitter.com/guillaumeclaret, https://foobar.land/)

Comme chaque fois, en remote, nous utiliserons Zoom (qui facilite les interactions) et les présentations seront suivies de ... notre fameux verre de l'amitié. Nous sommes très très impatient de vous retrouver le 10 Novembre ! Et encore merci à nos deux speakers !