2021 at OCamlPro

Authors: Muriel, OCamlPro

Date: 2022-01-31

Category: OCamlPro

Tags: OCamlPro, Highlights

OCamlPro was created in 2011 to advocate the adoption of the OCaml language and Formal Methods in general in the industry. 2021 was a very special year as we celebrated our 10th anniversary! While building a team of highly-skilled engineers, we navigated through our expertise domains, programming languages design, compilation and analysis, advanced developer tooling, formal methods, blockchains and high-value software prototyping.

In this article, as every year (see last year's post), we review some of the work we did during 2021, in many different worlds.

As always, we warmly thank all our clients, partners, and friends, for their support and collaboration during this peculiar year!

Newcomers at OCamlPro

A company is nothing without its employees. This year, we have been delighted to welcome a great share of newcomers:

• Hichem Rami Ait El Hara recently completed his master's degree in Computer Science. After an internship at OCamlPro, during which he developed a fuzzer for Alt-Ergo, he joined OCamlPro to work on Alt-Ergo and the verification of smart contracts. He will soon start a PhD on SMT solving.
• Nicolas Berthier holds a PhD on synchronous programming for resource-constrained systems. With many years experience on model-checking, abstract interpretation, and software analysis, he joined OCamlPro to work on programming language compilation and analysis.
• Julien Blond is a senior OCaml developer with a strong experience in formal verification of security software. He joined OCamlPro as both a project manager and a Coq expert.
• Keryan Didier joined the team as a R&D engineer. He holds a PhD from University Pierre et Marie Curie, during which he developed an automated implementation method for hard real-time applications. Previously, he studied functional programming and language design at University Paris-Diderot. Keryan has been involved in the MLang project as well as the flambda2 project within OCamlPro's Compilation team.
• Mohamed Hernouf recently completed his master's degree in Computer Science. After an internship at OCamlPro, working on the OCaml Documentation Hub, he joined OCamlPro and continues to work on the documentation hub and other OCaml applications.
• Dario Pinto is a student at the 42Paris School of Computer Science. He joined OCamlPro in a work-study contract for two years.
• Artemiy Rozovyk recently completed his master's degree in Computer Science. He joined OCamlPro to work on the development of applications for the EverScale and Avalanche blockchains.

Real Life Modern Applications

Modernizing the French Income Tax System

The M language is a very old programming language developed by the French tax administration to compute income taxes. Recently, Denis Merigoux and Raphael Monat have implemented a new compiler in OCaml for the M language. This new compiler shows better performance, clearer semantics, and achieves greater maintainability than the former compiler. OCamlPro is now involved in strengthening this new compiler, to put it in production and eventually compute the taxes of more than 30 million French families.

A First Step in the COBOL Universe

Born more than 60 years ago, COBOL is still said to be the most used language in the world, in terms of the number of lines running in computers, though many people forecast it would disappear at the edge of the 21st century. With more than 300 reserved keywords, it is also one of the most complex languages to parse and analyse. It's not enough to scare the developers at OCamlPro: while helping one of the biggest COBOL users in France to translate its programs into the GNUCobol open-source compiler, OCamlPro built a strong expertise of COBOL and mainframes, and developed a powerful parser of COBOL that will help us bring modern development tools to the COBOL developers.

Auditing a High-Scale Genealogy Application

Geneweb is one of the most powerful software to manage and share genealogical data to date. Written in OCaml more than 20 years ago, it contains a web server and complex algorithms to compute information on family trees. It is used by Geneanet, which is one of the leading companies in the genealogy field, to store more than 800,000 family trees and more than 7 billion names of ancestors. OCamlPro is now working with Geneanet to improve Geneweb and make it scale to even larger data sets.

Improving an ecotoxicology platform

The Mosaic platform helps researchers, industrials actors and regulators in the field of ecotoxicology by providing an easy way to run various statistical analyses. All the user has to do is to enter some data on the web interface, then computations are run on the server and the results are displayed. The platform is fully written in OCaml and takes care of calling the mathematical model which is written in R. OCamlPro modernised the project in order to ease maintainance and new contributions. In the process, we discovered bugs introduced by new R versions (without any kind of warning). Then we developped a new interface for data input, it's similar to a spreadsheet and much more convenient than having to write raw CSV. During this work, we had the opportunity to contribute to some other OCaml packages such as leveldb or write new ones such as agrid.

Contributions to OCaml

Flambda Code Optimizer

OCamlPro is proud to be working on Flambda2, an ambitious OCaml optimizing compiler project, initiated with Mark Shinwell from Jane Street, our long-term partner and client. Flambda focuses on reducing the runtime cost of abstractions and removing as many short-lived allocations as possible. Jane Street has launched large-scale testing of flambda2, and on our side, we have documented the design of some key algorithms. In 2021, the Flambda team grew bigger with Keryan. Along with the considerable amount of fixes and improvements, this will allow us to publish Flambda2 in the coming months!

In other OCaml compiler news, 2021 saw the long-awaited merge of the multicore branch into the official development branch. This was thanks to the amazing work of many people, including our own, Damien Doligez. This is far from the end of the story though, and we're looking forward to both further contributing to the compiler (fixing bugs, re-enabling support for all platforms) and making use of the features in our own programs.

This work is allowed thanks to Jane Street’s funding.

Opam Package Manager

Opam is the OCaml source-based package manager. The first specification draft was written in early 2012 and went on to become OCaml’s official package manager — though it may be used for other languages and projects, since Opam is language-agnostic! If you need to install, upgrade and manage your compiler(s), tools and libraries easily, Opam is meant for you. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.

Opam development and maintenance is a collaboration between OCamlPro, with Raja & Louis, and OCamlLabs, with David Allsopp & Kate Deplaix.

Our 2021 work on opam lead to the final release of the long-awaited opam 2.1, three versions of opam 2.0 and two versions of opam 2.1 with small fixes.

Opam 2.1 introduced several new features:

• Integration of system dependencies (formerly the opam-depext plugin)
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the "base packages" in opam 2.0 and allowing for easier compiler upgrades
• Improved option configurations
• CLI versioning, allowing cleaner deprecations for opam now and also improvements to semantics in future without breaking backwards-compatibility
• opam root readability by newer and older versions, even if the format changed
• Performance improvements to opam-update, conflict messages, and many other areas

Take a stroll through the blog post for a closer look.

In 2021, we also prepared the soon to-be alpha release of opam 2.2 version. It will provide a better handling of the Windows ecosystem, integration of Software Heritage archive fallback, better UI on user interactions, recursively pinning of projects, fetching optimisations, etc.

This work is greatly helped by Jane Street’s funding and support.

LearnOCaml and TryOCaml

We have also been active in the maintainance of Learn-ocaml. What was originally designed as the platform for the OCaml MOOC is now a tool in the hands of OCaml teachers worldwide, managed and funded by the OCaml Foundation.

The work included a well overdue port to OCaml 4.12; generation of portable executables (automatic through CI) for much easier deployment and use of the command-line client; as well as many quality-of-life and usability improvements following from two-way conversations with many teachers.

On a related matter, we also reworked our on-line OCaml editor and toplevel TryOCaml, improving its design and adding features like code snippet sharing. We were glad to see that, in these difficult times, these tools proved useful to both teachers and students, and look forward to improving them further.

OCaml Documentation Hub

As one of the biggest user of OCaml, OCamlPro aims at facilitating daily use of OCaml by developing a lot of open-source tooling.

One of our main contributions to the OCaml ecosystem in 2021 was probably the OCaml Documentation Hub at docs.ocaml.pro.

The OCaml Documentation Hub is a website that provides documentation for more than 2000 OPAM packages, among which of course the most popular ones, with inter-package documentation links! The website also contains browsable sources for all these packages, and a search engine to discover useful OCaml functions, modules, types and classes.

All this documentation is generated using our custom tool Digodoc. Though it's not worth a specific section, we also kept maintaining Drom, our layer on Dune and Opam that most of our recent projects use.

Pluging Opam into Software Heritage

Last year has also seen the long awaited collaboration between Software Heritage and OCamlPro happen.

Thanks to a grant by the Alfred P. Sloan Foundation, OCamlPro has been able to collaborate with our partners at Software Heritage and manage to further expand the coverage of this gargantuan endeavour of theirs by archiving 3516 opam packages. In effect, the main benefits of this Open Source collaboration have been:

• The addition of several modules to the Software Heritage architecture, allowing the archiving of said opam packages;
• The publication of an OCaml library allowing to work with SWHIDs;
• An implementation of a possible fallback onto Software Heritage if a given package on opam is no longer available;
• A fix for the official opam repository in order to identify already missing packages.

Not long after Software was at last acknowledged by Unesco as part of the World Heritage, we were thrilled to be part of this great and meaningful initiative. We could feel how true passion remained throughout our interactions and long after the work was done.

Tooling for Formal Methods

Alt-Ergo Development

OCamlPro develops and maintains Alt-Ergo, an automatic solver of mathematical formulas designed for program verification and based on Satisfiability Modulo Theories (SMT). Alt-Ergo was initially created within the VALS team at University of Paris-Saclay.

In 2021, we continued to focus on the maintainability of our solver. We released versions 2.4.0 and 2.4.1 in January and July respectively, with 2.4.1 containing a bugfix as well as some performance improvements.

In order to increase our test coverage, we instrumented Alt-Ergo so that we could run it using afl-fuzz. Although this is a proof of concept, and has yet to be integrated into Alt-ergo's continuous integration, it has already helped us find a few bugs, such as this.

Alt-Ergo Users’ Club and R&D Projects

We thank our partners from the Alt-Ergo Users’ Club, Adacore, CEA List, MERCE (Mitsubishi Electric R&D Centre Europe), Thalès, and Trust-In-Soft, for their trust. Their support allows us to maintain our tool.

The club was launched in 2019 and the third annual meeting of the Alt-Ergo Users’ Club was held in early April 2021. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo features and enhancements. If you want to join us for the next meeting (coming soon), contact us!

Finally, we will be able to merge into the main branch of Alt-Ergo some of the work we did in 2020. Thanks to our partner MERCE (Mitsubishi Electric R&D Centre Europe), we worked on the SMT model generation. Alt-Ergo is now (partially) able to output a model in the smt-lib2 format. Thanks to the Why3 team from University of Paris-Saclay, we hope that this work will be available in the Why3 platform to help users in their program verification efforts. OCamlPro was very happy to join the Why3 Consortium this year, for even more collaborations to come!

This work is funded in part by the FUI R&D Project LCHIP, MERCE, Adacore and with the support of the Alt-Ergo Users’ Club.

Dolmen Library for Automated Deduction Languages

Dolmen is a powerful library providing flexible parsers and typecheckers for many languages used in automated deduction.

The ongoing work on using the Dolmen library as frontend for Alt-Ergo has progressed considerably, both on the side of dolemn which has been extended to support Alt-Ergo's native language in this PR, and on Alt-Ergo's side to add dolmen as a frontend that can be chosen in this PR. Once these are merged, Alt-Ergo will be able to read input problems in new languages, such as TPTP!

Rust Developments

SMT, Induction and Mikino

A few months ago, we published a series of posts: verification for dummies: SMT and induction. These posts introduce and discuss SMT solvers, the notion of induction and that of invariant strengthening. They rely on mikino, a simple software we wrote that can analyze simple transition systems and perform SMT-based induction checks (as well as BMC, i.e. bug-finding). We wrote mikino in Rust with readability and ergonomics in mind: mikino showcases the basics of writing an SMT-based model checker performing induction. The posts are very hands-on and leverage mikino's high-quality output to discuss induction and invariant strengthening, with examples that readers can run and edit themselves.

Matla, a Project Manager for TLA+/TLC

During 2021 we ended up using the TLA+ language and its associated TLC verification engine in several completely unrelated projects. TLC is an amazing tool, but it is not suited to handle a TLA+ project with many modules (files), regression tests, etc. In particular, TLA+ is not a typed language. This means that TLA+ code tends to have many checks (dynamic assertions) checking that quantities have the expected type. This is fine, albeit a bit tedious, to some extent, but as the code grows bigger the analysis conducted by TLC can become very, very expensive. Eventually it is not reasonable to keep assert-type-checking everything since it contributes to TLC's analysis exploding.

As TLA+/TLC users, we are currently developing matla which manages TLA+ projects. Written in Rust, matla is heavily inspired by the Rust ecosystem, in particular cargo. Matla has not been publicly released yet as we are waiting for more feedback from early users. We do use it internally however as its various features make our TLA+ projects much simpler:

• handling the TLA toolchain (download, PATH, updates...) for the user;
• provide a Matla module with "debug assertions" helpers: these assertions are active in debug mode, which is the default when running matla run. Passing --release to matla's run mode however compiles all debug assertions away; this allows to type-check everything when debugging while making sure release runs do not pay the price of these checks;
• handle integration testing: matla projects have a tests directory where users can write tests (TLA files with a .tla and .cfg files) and specify if they are expected to be successful or to fail (and how);
• understand and transform TLC's output to improve user feedback, in particular when TLC yields an error (not good enough yet and is the reason we have not released yet); matla also parses and prettifies TLC's counterexample traces by formatting values, formatting states (aggregation of values), and render traces of states graphically using ASCII art.

Rust Training at Onera

The ongoing pandemic is undoubtingly impacting our professional training activities. Still, we had the opportunity to set up a Rust training session with applied researchers at ONERA during the summer. The session spanned over a week (about seven hours a day) and was our first fully remote Rust training session. We still believe on-site training (when possible) is better, full remote offers some flexibility (spreading out the training over several weeks for instance) and our experience with ONERA shows that it can work in practice with the right technology. Interestingly, it turns out that some aspects of the session actually work better with remote: hands-on exercises and projects for instance benefit from screen sharing. Discussing code with one participant is done with screen sharing, meaning all participants can follow along if they so chose.

Long story short, fully remote training is something we now feel confident proposing to our clients as a flexible alternative to on-site training.

Audit of a Rust Blockchain Node

We participated in a contest aiming at writing a high-level specification of the (compiler for) the TON VM assembler, in particular its instructions and how they are compiled. This contest was a first step towards applying Formal Methods, and in particular formal verification, to the TON VM. We are happy to report that we finished first in this context, and are looking forward to future contests pushing Formal Methods further in the Everscale blockchain.

Scaling and Verifying Blockchains

From Dune Network to FreeTON/EverScale

In 2019-2020, we concentrated our efforts on the development of blockchains on adding new programming languages to the Dune Network ecosystem, in collaboration with Origin Labs. You can read more about Love and Solidity for Dune.

At the end of 2020, it became clear that high-throughput was becoming a major requirement for blockchain adoption in real applications, and that the Tezos-based technology behind Dune Network could not compete with high-performance blockchains such as Solana or Avalanche. Following this observation, the Dune Network community decided to merge with the FreeTON community early in 2021. Initially developed by Telegram, the TON project was stopped under legal threats, but another company, TONLabs, restarted the project from its open-source code under the FreeTON name, and the blockchain was launched mid-2020. FreeTON, now renamed EverScale, is today the fastest blockchain in the world, with around 55,000 transactions per second on an open network sustained during several days.

EverScale uses a very unique community-driven development process: contests are organized by thematic sub-governances (subgov) to improve the ecosystem, and contestants win prices in tokens to reward their high-quality work. During 2021, OCamlPro got involved in several of these sub-governances, both as a jury, in the Formal Methods subgov and the Developer Experience subgov, and a contestant winning multiple prices for the development of smart contracts (zksnarks use-cases, auctions and recurring payments), the audit of several smart contracts (TrueNFT audit, Smart Majority Voting audit and a DEX audit), and the specification of some Rust components in the node (the Assembler module).

This work in the EverScale ecosystem gave us the opportunity to develop some interesting OCaml contributions:

• We improved our ocaml-solidity parser to support all the extensions of the Solidity language required to parse EverScale contracts;
• We developed an OCaml binding for the EverScale Rust SDK;
• We developed a command line wallet called ft to help developers easily deploy the contracts and interact with them;
• We developed a bridge between Dune Network and EverScale to swap DUN tokens into EVER tokens.

This work was funded by the EverScale community through contests.

A Why3 Framework for Solidity

Our most recent work on the EverScale blockchain has been targetted into the development of a Why3 framework to formally verify EverScale Solidity contracts. At the same time, we have been involved in the specification of several big smart contract projects, and we plan to use this framework in practice on these projects as soon as their formal verification starts.

We hope to be able to extend this work to EVM based Solidity contracts, as available on Ethereum and Avalanche and many other blockchains. By comparison with other frameworks that work directly on the EVM bytecode, this work focused directly on the Solidity language should make the verification much higher-level and so more straight-forward.

Participations in Public Events

Open Source Experience 2021

We were present at the new edition of the Open Source Experience in Paris! Our booth welcomed our visitors to discuss tailor-made software solutions. Fabrice had the opportunity to give a presentation on FreeTON (Now EverScale) (Watch the video), the high speed blockchain he is working on. We were delighted to meet the open source community. Moreover, Amélie de Montchalin, French Minister of Transformation and Public Service, was present to the Open Source Experience to thank all the free software actors. A very nice experience for us, we can't wait to be back in 2022!

OCaml Workshop at ICFP 2021

We participated in the programming competition organized by the International Conference on Functional Programming (ICFP). 3 talks we submitted to the OCaml Workshop were accepted!

• Fabrice, Mohamed and Louis presented Digodoc, our new tool that builds a graph of an opam switch, associating files, libraries and opam packages into a cyclic graph of inclusions and dependencies;
• Fabrice spoke about Opam-bin, a plugin that builds binary opam packages on the fly;
• Lastly, Steven and David presented Love, a smart contract language embedded in the Dune Network blockchain. It was an opportunity to present our tools and projects, and above all to discuss with the OCaml community. We're delighted to take part in this adventure every year!

Joining the Why3 Consortium at the ProofInUse seminar

We were very happy to join the Why3 Consortium while participating the ProofinUse joint lab seminar on counterexamples on October the 1st. Many thanks to Claude Marché for his role as scientific shepherd.

Towards 2022

After a phase of adaptation to the health context in 2020 and a year of growth in 2021, we are motivated to start the year 2022 with new and very enriching projects, new professional encounters, leading to the growth of our teams. If you want to be part of a passionate team, we would love to hear from you! We are currently actively hiring. Check the available job positions and follow the application instructions!

All our amazing achievements are the result of incredible people and teamwork, kudos to Fabrice, Pierre, Louis, Vincent, Damien, Raja, Steven, Guillaume, David, Adrien, Léo, Keryan, Mohamed, Hichem, Dario, Julien, Artemiy, Nicolas, Elias, Marla, Aurore and Muriel.

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

• We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, Wasm and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
• We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we helped the French Income Tax Administration re-adapt and improve their internally kept M language, we designed a DSL to model and express revenue streams in the Cinema Industry, codename Niagara, and we also developed the prototype of the Tezos proof-of-stake blockchain from 2014 to 2018.
• We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
• We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.