[Interview] Sylvain Conchon joins OCamlPro

---

On April 2020, Sylvain Conchon joined the OCamlPro team as our Chief Scientific Officer on Formal Methods. Sylvain is a professor at University Paris-Saclay, he has also been teaching OCaml in universities for about 20 years. He is the co-author of Apprendre à programmer avec OCaml with Jean-Christophe Filliâtre, a book for students in French elitist Preparatory Schools. His field of expertise is the automated deduction for program verification and model checking of parameterized systems. He is also the co-creator of Alt-Ergo, our SMT Solver dedicated to program verification, used by Airbus and qualified for the [DO-178C](http://(https://en.wikipedia.org/wiki/DO-178C) avionic standard, of Cubicle and the very useful OCamlgraph library.

Research and Industry

Sylvain, you’ve been involved in the industrial world for a long time, what do you think about the interactions between industry and research labs?

I’ve always found interactions with industry professionals to be very rewarding. During my studies, I worked for several years in IT (SSII), and as a university professor, I have supervised students during their internships or apprenticeships in tech companies or at large industrial companies every year. I also take part in research projects that involve industrial partners, and I spent some time at Intel in Portland, which allowed me to discover the computer hardware industry from inside.

How do you establish a fruitful collaboration between academia and industry?

It’s primarily a question of mutual understanding. You can see it clearly during collaborative research projects that involve both academics and industrial partners. Tools resulting from research, no matter what they are, have to be relevant to real industrial problems. Once that’s taken care of, the software also needs to be usable by industry professionals without them needing to understand its inner workings (for instance they shouldn’t have to specify all 50 necessary options for its use, interpret its results, or its absence of results!).

This requires a significant engineering effort geared towards the end user; and this task is not part of usual research activity. So, we first need to really understand the problems and needs of the industrial partner, and then determine whether our technologies and tools can be adapted or used to prototype a relevant solution.

You’ve just joined OCamlPro, what are your first thoughts?

I am very happy to be joining such a dynamic company full of talented, motivated, friendly people, where they do both high-level engineering and top-quality research! Several of my former PhD students are also working at OCamlPro, such as Albin Coquereau, David Declerck and Mattias Roux. With Mohamed Iguernlala and Alain Mebsout at our partner Origin Labs, and with the other OCP team members, it makes our team rock-solid in formal methods tooling development.

“Tools resulting from research, no matter what they are, have to satisfy real industry needs.”

OCaml, a Cutting-Edge Language

You are well known in the OCaml community, and some of your students became fans of OCaml (and of your teaching)… What do you say to your students who are just discovering OCaml?

I tend to summarize it with one phrase: “With OCaml, you’re not learning the computer programming of the last 10 years, you’re learning the programming of the 10 coming years”. This has proven true numerous times, because a good number of OCaml’s features were to be found in mainstream languages years later. That being said, all my years of teaching this language have led me to think that some modifications to its syntax would make the language easier to tackle for some beginners.

How did you personally discover OCaml?

During my master’s thesis (maîtrise) at university: one of my teachers pointed this language to me; they believed it would help me write a compiler for another programming language. So, I discovered OCaml by myself, by reading the manual and going through examples. It wasn’t until my MASt (DEA) that I discovered the theoretical foundations of this fantastic language (semantics, typing, compilation).

Would you say OCaml is an industrial programming language?

The question needs to be clarified: what is an industrial programming language? If by industrial language you mean one that is used by industry professionals, then I’d say that OCaml needs to be used more widely to be classified as such. If the question is whether OCaml is at the same level as languages used in industry, then it absolutely is. But maybe the question is more about the OCaml ecosystem and how developed the available tooling is: certain improvements undoubtedly need to be made in order to reach the level of a widespread industrial programming language. But we’re on the right track, especially thanks to companies like OCamlPro and its projects like Opam and Try-OCaml for example.

Formal Methods as an Industrial Technique, and the Example of the Alt-Ergo Solver

Formal methods being one of OCamlPro’s areas of expertise, in what way do you think OCaml is suited for the SMT domain?

Tools like SMT solvers are mainly symbolic data manipulation software that allow you to analyze, transform, and reason about logical formulas. OCaml is made for that. There is also a more “computational” side to these tools, which requires precise programming of data structures as well as efficient memory management. OCaml, with its extremely efficient garbage collector (GC), is particularly suited for this kind of development. SMT solvers are tools that also need to be very reliable because errors are difficult to find and are potentially very harmful. OCaml’s type system contributes to the reliability of these tools.

“SMT solvers are nowadays essential in software engineering”

Can you describe Alt-Ergo in a few words?

Alt-Ergo is a software for proving logical formulas automatically (without human intervention), meaning proving whether a formula is true or false. Alt-Ergo belongs to a family of automated provers called SMT (Satisfiability Modulo Theories). It was designed to be integrated into program verification platforms. These platforms (like [Why3](https://(https://why3.lri.fr/), Frama-C, Spark…) generate logical formulas that need to be proven in order to guarantee that a program is safe. Proving these formulas by hand would be very tedious (there are sometimes tens of thousands of formulas to prove). An SMT solver such as Alt-Ergo is there to do that job in a completely automated way. It is what allows these verification platforms to be used at an industrial level.

In what way developing this software in OCaml benefits Alt-Ergo over its competitors?

It makes it more reliable, since an SMT solver, like any program, can have bugs. Most of Alt-Ergo is written in a purely functional programming style, i.e. only using immutable data structures. One of the advantages of this programming style is that it allowed us to formally prove the main components of Alt-Ergo (for example, its kernel was formalized using the Coq proof assistant, which would have been impossible with a language like C++) without sacrificing efficiency thanks to a very good garbage collector and OCaml’s very powerful persistent data structure library. We made use of OCaml’s module system, particularly functors and recursive modules, to conceive a very modular code, making it maintainable and easily extensible. OCaml allowed us to create an SMT solver just as efficient as CVC4 or Z3 for program verification, but with a total number of lines of code divided by three or four.This obviously does not guarantee that Alt-Ergo has zero bugs, but it really helps us in fixing any if they are found.

What is your opinion on SMT solvers and the current state of the art of SMT?

Today, SMT solvers are essential in software engineering. They can be found in various tools for proving, testing, model checking, abstract interpretation, and typing. The main reason for this success is that they are becoming increasingly efficient and the underlying theories are becoming more and more expressive. It is a very competitive area of research among the world’s best universities and research labs, as well as large IT companies. But there is still a lot of room for improvement, particularly in the nonlinear arithmetic domain, where user demand is growing. For now, one of my research objectives is to combine Model Checking tools with program verification. These two types of tools are based on SMT and should complement each other to offer even more automation to verification tools.

What applications can SMT techniques and Alt-Ergo have in industry?

SMT techniques can be used wherever formal methods are useful. Including, but not limited to verifying the safety of critical software in embedded systems, finding security vulnerabilities in computer systems, or resolving planning problems. They can also be found in domains of artificial intelligence, where it is crucial to guarantee neural network stability and produce formal explanations of their results.

You ended up working on Model Checking, can you tell us about how Model Checking is connected to SMT and how it is currently used?

Model Checking consists of verifying that all possible states of a system respect certain properties, regardless of the input data. This is a difficult problem because some systems (like microprocessors for example) can have hundreds of millions of states. To reach that scale, model checkers implement extremely sophisticated algorithms to visit these states quickly by storing them in a compact manner. That said, this technique reaches its limits when the input values are unbounded or when the number of system components is unknown. Imagine Internet routing algorithms where you don’t know how many machines are connected. These algorithms must be correct no matter the number of machines. This is where SMT solvers come into play. By using logical formulas, we’re able to represent sets of states of arbitrary sizes. Visiting system states becomes calculating the formulas that represent the states satisfying the desired properties, etc. Therefore, everything in Model Checking is based on logical formulas, and SMT solvers are of course there to reason about these formulas.

---

Au sujet d'OCamlPro :

OCamlPro développe des applications à haute valeur ajoutée depuis plus de 10 ans, en utilisant les langages les plus avancés, tels que OCaml et Rust, visant aussi bien rapidité de développement que robustesse, et en ciblant les domaines les plus exigeants (méthodes formelles, cybersécurité, systèmes distribués/blockchain, conception de DSLs). Fort de plus de 20 ingénieurs R&D, avec une expertise unique sur les langages de programmation, aussi bien théorique (plus de 80% de nos ingénieurs ont une thèse en informatique) que pratique (participation active au développement de plusieurs compilateurs open-source, prototypage de la blockchain Tezos, etc.), diversifiée (OCaml, Rust, Cobol, Python, Scilab, C/C++, etc.) et appliquée à de multiples domaines. Nous dispensons également des [formations sur mesure certifiées Qualiopi sur OCaml, Rust, et les méthodes formelles] (https://training.ocamlpro.com/) Pour nous contacter : contact@ocamlpro.com.