> Sylvain Conchon vient de rejoindre OCamlPro en tant que Chief Scientific Officer Méthodes Formelles. Professeur à l’Université Paris-Saclay, il travaille dans le domaine de la démonstration automatique pour la preuve de programmes et le model checking pour systèmes paramétrés. Il est aussi le co-créateur d’Alt-Ergo.
### Recherche et industrie
**Sylvain, tu fréquentes de longue date le monde industriel,
que penses-tu des interactions entre les industriels et les laboratoires
de recherche ?**
J’ai toujours trouvé très enrichissantes les interactions avec les
industriels. Pendant mes études, j’ai travaillé plusieurs années en
SSII, et je suis mes étudiants en stage ou en apprentissage dans des
sociétés technologiques ou chez de grands industriels. Je participe
également à des projets de recherche qui impliquent des industriels,et
j’ai passé quelques temps chez Intel à Portland, ce qui m’a permis de
découvrir l’industrie du hardware.
**Comment parvenir à établir des relations fructueuses entre le monde académique et les industriels ?**
C’est beaucoup une histoire de rencontre. On le voit lors des
montages de projets de recherche collaboratifs qui réunissent
académiques et industriels. Les outils issus de la recherche, quels
qu’ils soient, doivent avant tout répondre à un besoin réel des
industriels. Si c’est le cas, il faut aussi que le logiciel soit
utilisable par des ingénieurs du métier sans qu’il leur soit nécessaire
de comprendre son fonctionnement interne (par exemple, pour positionner
les 50 options nécessaires à son utilisation, interpréter ses résultats
ou ses absences de résultats!). Cela nécessite à l’évidence un travail
d’ingénierie important, tourné vers l’utilisateur final et souvent
éloigné des activités des chercheurs. Il faut donc comprendre les
problèmes et les besoins des industriels, et ensuite déterminer si les
technologies et les outils que l’on maîtrise peuvent être adaptés ou
utilisés pour réaliser un prototype qui réponde à certains de ces
besoins.
**Tu viens de rejoindre OCamlPro, quelles sont tes premières impressions ?**
Je suis heureux d’avoir rejoint une entreprise très dynamique, pleine
de gens talentueux, motivés et sympathiques, où l’on fait à la fois de
l’ingénierie de haut niveau et de la recherche de qualité !
> *“ Les outils issus de la recherche, quels qu’ils soient, doivent avant tout répondre à un besoin réel des industriels.”*
### OCaml, un langage de pointe
**Tu es connu dans la communauté OCaml, et certains de
tes étudiants sont devenus des fans d’OCaml (et de ton enseignement)…
que dis-tu à tes étudiants qui découvrent OCaml ?**
J’ai tendance à résumer en disant ceci : *« avec OCaml, vous n’apprenez pas la programmation des 10 dernières années, mais celle des 10 prochaines années »*. Cette affirmation s’est toujours vérifiée car bon nombre de traits du langage OCaml se sont retrouvés dans les langages *mainstream*, avec plusieurs années de décalage. Cela dit, mes années d’expérience dans l’enseignement de ce langage me laissent penser que quelques modifications dans sa syntaxe permettraient une approche plus aisée pour certains débutants.
**Et toi, comment as-tu découvert OCaml ?**
Pendant mes études à l’Université lors de mon projet de fin de
maîtrise : un de mes enseignants m’avait orienté vers ce langage pour
m’aider à réaliser un compilateur pour un langage de programmation
concurrente. J’ai donc découvert ce langage par moi-même, en lisant le
manuel et les exemples. Ce n’est que pendant mon DEA que j’ai découvert
les fondements théoriques de ce beau langage (sémantique, typage,
compilation).
**OCaml, un langage industriel ou pas encore ?**
Il convient de préciser la question : qu’est-ce qu’un langage
industriel ? Si c’est un langage utilisé par les industriels, alors
OCaml n’est hélas pas encore suffisamment utilisé dans l’industrie pour
être qualifié ainsi. Si la question est de savoir s’il a le niveau des
langages utilisés dans l’industrie, alors la réponse est oui, sans
hésiter. Mais peut-être la question porte-t-elle davantage sur
l’écosystème OCaml et la maturité de l’outillage: il y a sûrement des
progrès à faire pour atteindre le niveau d’un langage très répandu dans
l’industrie, mais c’est en bonne voie, en particulier grâce à des
entreprises telles qu’OCamlPro.
### Les méthodes formelles comme technique industrielle, et l’exemple du solveur Alt-Ergo
**Les méthodes formelles sont l’un des domaines d’expertise d’OCamlPro, en quoi penses-tu qu’OCaml est adapté au domaine des SMT ?**
Les outils comme les solveurs SMT sont principalement des logiciels
de manipulation symbolique des données qui permettent d’analyser, de
transformer et de raisonner sur des formules logiques. OCaml est fait
pour ce genre de traitements. Il y a aussi une partie plus «
calculatoire » dans ces outils qui nécessite une programmation fine des
structures de données ainsi qu’une gestion efficace de la mémoire. OCaml
est particulièrement adapté pour ce genre de développements, surtout
avec son ramasse-miettes (GC) extrêmement performant. Enfin, les
solveurs SMT sont des outils qui doivent avoir un grand niveau de
fiabilité car les erreurs dans ces logiciels sont difficiles à trouver
et leur présence peut être très préjudiciable. Le système de types
d’OCaml contribue à la fiabilité de ces outils.
> *“Les solveurs SMT sont aujourd’hui incontournables dans le domaine de l’ingénierie du logiciel.”*
**Peux-tu nous parler d’Alt-Ergo en quelques mots ?**
C’est un logiciel utilisé pour prouver automatiquement (sans
intervention humaine) des formules logiques, c’est-à-dire savoir si ces
formules sont vraies ou fausses. Alt-Ergo appartient à une famille de
