2022 at OCamlPro

---

For 12 years now, OCamlPro has been empowering a large range of customers, allowing them to harness state-of-the-art technologies and languages like OCaml and Rust. Our not-so-small-anymore company steadily grew into a team of highly-skilled and passionate engineers, experts in Computer Science, from Compilation and Software Analysis to Domain Specific Languages design and Formal Methods.

In this article, as every year (see last year's post) - albeit later than we do usually, we review some of the work we did during 2022, in many different worlds as shows the wide range of the missions we achieved.

Newcomers at OCamlPro

OCamlPro is not just a R&D software company, we like to think about it more as a team of people who like to work together. So, we are proud to introduce you the incredible human beings that joined us in 2022:

• Pierre Villemot joined us in June. After three years of research at the Weizmann Institute on transcendental measures in Arithmetical Geometry, he was recruited and became the main maintainer of the Alt-Ergo Theorem Prover.

• Milàn Martos joined us in July. He studied Chemistry and Computer Science at ENS, and he holds an MBA. He joined the Team as a Presales Engineer and as a Junior OCaml Web Developer.

• Nathanaëlle Courant joined us in September. She holds a Master's degree from École Normale Supérieure in Paris, and is finishing her Ph.D. on efficient and verified reduction and convertibility tests for theorem provers. She joined OCamlPro in 2022 and works on the OCaml optimizer, in the Flambda team.

• Arthur Carcano also joined us in September. Arthur is a Rust developer interested in performance optimization, software design, and crafting powerful and user-friendly tools. After completing his M.Sc. in Computer Science at ENS Ulm, he obtained a Ph.D. in Mathematics and Computer Science from Université de Paris.

• Emilien Lemaire joined us in December 2022. After an internship on typechecking COBOL statements, he will be working with our COBOL team on creating a studio of modern tools for COBOL.

Modernizing Core Parts of Real Life Applications

We love to harness our IT expertise to give a competitive advantage to our clients by modernizing core chunks of key infrastructures. For example, we are working with the French Public Finances General Directorate on two of their modernization projects, to reimplement the language used for the computation of the Income Tax (MLang) and to provide support on the GnuCOBOL compiler used by the MedocDB application (COBOL).

MLANG, keystone of the French citizens' Income Tax Calculation

In 2022, our work on MLANG has passed a significant milestone: our work may no longer be considered a prototype! Code generation is now behaviourly compliant with the upstream compiler. David focused on rewriting the C architecture, which has been of great aid in iterating through each version of this new implementation of MLANG.

As far as testing goes, we were allowed to compare the results of our implementation against the ones of the upstream calculator, on real-life inputs too. We are talking about calculations of immense scale, which entails a highly performance-dependent project. Naturally, we managed to produce something of equivalent performance which was a very important matter for our contractors which have, since then, voiced their satisfaction. It is always great for us to feel appreciated for our work.

The next step is to make a production-level language by the end of 2023, so stay tuned if you are interested in this great project.

Wondering what MLANG is ? Be sure to read last year's post on the matter.

Contributing to GnuCOBOL, the Free Open-Source COBOL Alternative

In 2022, we started contributing to the GnuCOBOL project: the GnuCOBOL compiler is, today, the only free, open-source, industrial-grade alternative to proprietary compilers by IBM and Micro-Focus. A cornerstone feature of GnuCOBOL is its ability to understand proprietary extensions to COBOL (dialects), to decrease the migration work of developers.

Last year's at OCamlPro presented our gradual introduction to the COBOL Universe as one of our latest technical endeavours. In the beginning, our main objective was to wrap our heads around the state of the environment for COBOL developers.

Our main contribution for now is to add support for the GCOS7 dialect, to ease migration from obsolete GCOS Bull mainframes to a cluster of PCs running GnuCOBOL for our first COBOL customer, the French DGFIP (Public Finances General Directorate). We also contributed a few fixes and small useful general features. Our contributions are gradually upstreamed in the official version of GnuCOBOL.

The other part of our COBOL strategy is to progressively develop our SuperBOL Studio, a set of modern tools for COBOL, and especially GnuCOBOL, based on an OCaml parser for COBOL that we have been improving during the year to support the full COBOL standard. More on this next year, hopefully !

Rust Expertise and Developments

OCamlPro's culture is one of human values and appeal for everything scientific.

Programming languages of all nature have caught our attention at some point in time. As a consequence of years of expertise in all kinds of languages, we have grown fond of strongly-typed, memory-safe ones. Eventually gravitating towards Rust, we have since then invested significantly in adding this state-of-the-art language to our toolsets, one of which being the trainings we deliver to industrial actors of various backgrounds to help them grasp at such technological marvels.

Our trainers are qualified engineers, some of which have more than ten years of experience in the industry in R&D, Formal Methods and embedded systems alike, seven of which being solely in Rust.

Strong of our collective experiences, 2022 was indeed the stage for many contributions and missions, some of which we will share with you right now.

Ecore, a heart of Rust for EMF

In 2022, we have seized the opportunity to work at the threshold between Java and Rust for our clients and academic partners of the CEA (Commissariat aux Énergies Atomiques et aux Énergies Alternatives). The product was a Rust-written and Rust-encoded Java class hierarchy code generator.

Ecore is the core metamodel at the heart of the Eclipse Modeling Framework (EMF), which is used internally at the CEA. Ecore is a superset of UML and allows for the engineers of the CEA to express a Java class hierarchy through a graphical interface. In practice, this allows for the generation of basic Java models for the engineers to then build upon.

Our mission consisted in writing, in Rust, a new model generator for them to use in their workflows and to make it capable of generating Rust code instead of Java.

The cost for harnessing the objective qualities of a new implementation in Rust was to have us tackle the scientific challenges pertaining to the inherent structural differences between both languages. Our goal was to find a way to encode, in Rust, a way to express the semantics of the hierarchy of classes of Java, hence merging the worlds of Rust and Java on the way there.

Eventually, our partners were convinced the challenges were worth the improved speed at which models were generated. Furthermore, the now embedded-programming compliant platform, the runtime safety and even Rust's broader WebAssembly-ready toolchain have cleared a new path for the future iterations of their internal projects.

Open-Source Rust Contributions

As we continue scouring the market for more and more Rust projects, and whenever the opportunity shows up, we still actively contribute to the open-source community, here are some of this year's OS work:

Lean4

Here's a project suited for all who, like us, are Formal Methods, functional programming and formal methods enthousiasts: Lean:

Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming.

The list of our contributions to the repository of lean4:

• Detection of a major dependent pattern matching bug
• Some QA with unintuitive calc indentation
• And some more with strict indentation in nested by-s requirement

Matla, TLA+ Projects Manager

Last year, we shared a sneakpeek of Matla, introducing its use-case and the motivations for implementing such manager for TLA+ projects. As we tinkered with TLA+, sometimes finding a bug, we continued our development of Matla on the side.

The tool, although still a work-in-progress, has since then undergone a few changes and releases:

• Implemented user feedback
• Clap builder overhaul
• Fixed a bug in temporal (lasso) cex parsing
• Documentation efforts
• Fix double quote parsing and no JRE error

You are welcome to contribute if you happen to find yourself in the same situation we were in when we started the project.

Agnos, for Let's Encrypt Wildcard Certificates

Agnos is a single-binary program allowing you to easily obtain certificates (including wildcards) from Let's Encrypt using DNS-01 challenges. It answers Let's Encrypt DNS queries on its own, bypassing the need for API calls to your DNS provider, and strives to offer a user-friendly and easy configuration.

Often, the best contributions are of a practical nature, which is the case for Agnos.

If that sounds interesting to you, you can learn more about it by reading this article.

Make sure to give us some feedback when you end up using it!

The WebAssembly Garbage Collection Working-Group

Late 2022 was finally time for us to put into practice the knowledge we have acquired about WebAssembly over the years by writing and presenting the first compiler of a real-world functional language targeting the WasmGC proposal.

Although a relatively new technology, its great design, huge potential, and already very tangible and interesting use-cases have not escaped our watch and we are very happy to have kept a sharp eye on it.

WebAssembly (abbreviated Wasm) is a binary instruction format for a stack-based virtual machine. Wasm is designed as a portable compilation target for programming languages, enabling deployment on the web for client and server applications.

WasmGC is the name of the on-going working group and proposal towards eventually adding support for garbage collection to Wasm. December 2022 saw a significant amount of work accomplished by both Léo Andrès (whose thesis work is directed by Pierre and Jean-Christophe Filliâtre) and Pierre Chambart towards finding viable compilation strategies from OCaml to WasmGC. The goal was three-fold: make a prototype compiler to demonstrate the soundness of the proposal, show that our compilation strategies were viable and, finally, convince the commitee of the significance of the Wasm i31ref for OCaml.

Our success in these three distinct points was paramount for OCaml, and other languages that depend on the presence of i31ref, in order to one day benefit from having WebAssembly as a natively supported compilation target for Web-bound applications.

Here's a short listing of the work they have accomplished for that matter. Please rest assured, more detailed explanations are to be expected on this very blog in the future so stay tuned!

• Introducing Wasocaml to the Wasm-GC Group and demonstrating the OCaml's dependency on Wasm keeping i31ref in their GC proposal.
• Wasocaml, an OCaml compiler to Wasm. Wasocaml is also the first compiler for a real-world functional language to Wasm-GC.
• owi, an OCaml toolchain to work with Wasm. It provides and interpreter as an executable and a library.

Tooling for Formal Methods

Programming languages theory is closely tied with the idea of proper mathematical formalisation. Hence the strong scientific background in Formal Methods that we draw from both for language design or formal verification for cybersecurity.

The Alt-Ergo Theorem Prover

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

The Alt-Ergo Users' Club

The Alt-Ergo Users' Club was launched in 2019. Its 4th annual meeting was held in late March 2022.

These meetings allow us to keep track of our members' needs and demands as well as keep them informed with the latest changes to the SMT Solver; they are the lifeline of our Club and help us guarantee that the project lives on, despite the enormous task it represents.

This is a good time to appreciate the scope of the project: Alt-Ergo is the fruit of more than 10 years' worth of Research & Development. Currently maintained by Pierre Villemot, whom we will introduce in the next section, as full-time R&D engineer.

This is the reason why we would like to thank our partners from the Alt-Ergo Users’ Club, for their trust: Thales, Trust-in-Soft, AdaCore, MERCE (Mitsubishi Electric R&D Centre Europe) and the CEA. Their support allows us to maintain our tool.

Congratulations and many thanks to our partners at Trust-In-Soft, who have upgraded their subscription to the Club to Gold-tier, allowing this great open-source tool to live on!

Developing Alt-Ergo

In 2022, the Alt-Ergo team welcomed Pierre Villemot as full-time maintainer of the project! His recruitement shows our commitment to the project's long term maintenance and evolution. We are looking forward to seeing him take it to new heights in future releases! Speaking of releases, 2022 has also been the stage for Alt-Ergo's v2.4.2 minor release which introduced an update of the labgltk library to version 3 and a set of bug fixes.

Now onto the more substantial changes to Alt-Ergo, the integration into next of all the following:

• Integration of the SMT-LIB2 format parser Dolmen to Alt-Ergo's frontend;
• Improvement and test of models generation;
• Addition of mutually recursive functions for the legacy frontend and Dolmen alike;
• Significant amounts of documentation and code-cleaning;
• Implementation of systematical benchmarks of the SMT-LIB for regression prevention;
• Prototypical Dockerisation;

These are significative improvements to the User Experience and overall ergonomy of the tool. You can already benefit from these changes by using Alt-Ergo's dev version.

Finally, let us inform you that our candidacy for the DECYSIF project was approved. Indeed, we and our partners at Adacore, Trust-In-Soft and the Laboratoire Méthodes Formelles have been selected to conduct this funded research project as consultant in Formal Methods. Now, we hope to be part of collaborative R&D projects to further fund core Alt-Ergo developments. This should allow us to deepen collaboration with old partners like the Why3 team at the Formal Methods Lab (LMF) and the ProofinUse consortium members. Stay tuned!

Dolmen Library for Automated Deduction Languages

Dolmen is an OCaml Library developed by Guillaume Bury as part of our Research and Development processes around Formal Methods and our development efforts for our automated SMT-Solver Alt-Ergo.

Dolmen is a testimony of our push towards standardised input languages for SMT-Solvers. Indeed, it provides flexible Menhir parsers and typecheckers for several languages used in automated deduction such as: smtlib, ae (Alt-Ergo), dimacs, iCNF, tptp and zf (zipperposition). And so, Dolmen aims at encompassing the largest amount of input languages for automated deduction as possible and provides the OCaml community with a centralised solution for their input parsing and typechecking, hence keeping them from having to reimplement them each time.

Furthermore, the Dolmen binary is used by the maintainers of the SMTLIB in order to assert that newly submitted benchmarks to the SMTLIB are compliant with the specification which makes Dolmen its de facto reference implementation. In time, Dolmen will become the default frontend for Alt-Ergo and, we hope, any other OCaml written SMT-Solver from now on.

Contributions to OCaml

Last but not least, OCamlPro’s DNA built itself on one of the most powerful and elegant programming languages ever, born from more than 30 years of French public Research in Computer Science, and widely used in safety critical industries. OCaml’s traits pervasively inspired many new languages (like F#). We are proud to be part of this great community of researchers and computer scientists.

About opam, the OCaml Package Manager

2022 has been the theatre of a sustained and continuous effort from the opam team.

The fruits of their labor have been compiled into an alpha release of version 2.2.0 by June 28th 2023, so here is a taste of what should make the final 2.2.0 version of opam a treat for its users:

• Windows support: opam 2.2 comes with native Windows compatibility. You can now use opam from your preferred Windows terminal!
• Recursive pinning: allows to have opam lookup for opam files into subdirectories.
• Software Heritage binding: opam now integrates a fallback to Software Heritage archive retrieval, based on SWHID. If an SWHID url is present in an opam file, the fallback can be activated.
• Enhanced features for developers: as the development tools variable to share a development setup, the opam tree command to have better an overview of dependencies, new pinning subcommands, and so on.

That being said, 2022 was a very special year for opam. Indeed, 10 years prior, on the 26th of June 2012, OCamlPro birthed version 0.1 of what was to become the official OCaml Package Manager, the cornerstone of the OCaml environment.

It was no small feat to make opam what it is today. It took approximately 5 years to bring 1.0.0 up to 2.0.0 and another 3 to reach 2.1.0 all the while ensuring changes were compliant with the current ecosystem (opam repository, OCaml tooling) and the public's feedback and vision.

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

The Flambda2 Optimizing Compiler

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. Flambda2 builds upon its predecessor: Flambda, which focused on reducing the runtime cost of abstractions and removing as many short-lived allocations as possible. Thus, Flambda2 not only shines with the maturity and experience its architects acquired through years worth of R&D and dev-time for Flambda, but it improves upon them.

In 2022, Flambda2 was for the first time used for production workloads and has been ever since! Indeed, we can officially say that Flambda2 left the realm of the prototype to enter one of real-life, production-tested software for which we continue to provide development and support as it has been for years now.

This achievement comes along having our engineers take more and more action in maintaining the OCaml compiler. Being part of the OCaml Core-Team is an honour.

Finally, in 2022, the Flambda Team welcomed a new member: Nathanaëlle Courant will be joining forces with Pierre Chambart, Damien Doligez, Vincent Laviron, Guillaume Bury to tackle the challenges inherent to maintaining Flambda2 and that of the Core-Team.

If you are interested in more things Flambda2, stay tuned in with our blog, there should be a series of very interesting articles coming up in the not-so distant future!

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

In other OCaml compiler news, 2022 was also the year of the official release of OCaml 5.0.0, also known as Multi-Core, on the 16th of December. This major release introduced a new runtime system with support for shared memory parallelism and effect handlers! This fabulous milestone is brought to us by the joined work of the amazing people of the OCaml Core-Team; among them some of our own.

Many thanks to all who take part in uncovering the yet untrodden paths of the OCaml distribution!

What a time to be an OCaml enthousiast!

Organizing Meetups for the OCaml Community

OCaml Users in PariS (OUPS)

Just under 10 years ago, Fabrice Le Fessant initiated the very first OCaml Users in Paris.

This event allowed OCaml users in Paris, professionals and amateurs alike, to meet and exchange on OCaml novelties. This is still the case and the organising crew now includes several people of diverse affiliations, maintaining the purpose of this friendly event.

Every two months or so, the organisers reach out to the community, hail volunteers and select presentations of on-going works. When the time and place is settled, the ocaml-paris Meetup members are informed by various means. The OCaml Users in PariS meetup is the place to enthusiastically share knowledge and a few pizzas. It is supported by the OCaml Software Foundation who graciously pays for the pizzas.

You can register to the OCaml Users in PariS (OUPS) meetup group here.

Here are all the relevant links to the talks that happened in Paris in 2022:

• 10th March 2022
• 12th May 2022
• 29th September 2022
• 8th December 2022

OCaml Meet-Up in Toulouse

Fortunately for OCaml Users that live in the French South-West, a new Meet-up is now available to them. On the 11th of October 2022, the first OCaml meet-up in Toulouse happened.

The first occurence of the OCaml Users in Toulouse Meetup kicked off with Erik Martin-Dorel (OCaml Software Foundation) presenting Learn-OCaml who was then followed by David Declerck (OCamlPro) presenting his OCaml-Canvas graphics library for OCaml.

You can register to the OCaml Meet-Up in Toulouse group here.

Here's to sharing a slice or two with you soon!

Participation to External Events

The OCaml Workshop 2022 - ICFP Ljubljana

The OCaml Workshop is an international conference that focuses on everything OCaml and is part of the ICFP (International Conference on Functional Programming).

We attended many of these and have presented numerous papers throughout the years.

In 2022, a paper co-authored by the maintainers of opam, the OCaml Package Manager, was submitted and approved for presentation: "Supporting a decade of opam".

You can find the textual references of the talk here and a replay of the presentation there.

You can expect more papers and interesting talks coming from us in upcoming editions of the conference!

Journées Francophones Langages Applicatifs 2022

Among the many scientific conferences we attend on an annual basis, the JFLA (Journée Francophones des Langages Applicatifs or French-Speaking annual gathering on Application Programming Languages, mainly Functional Languages) is the one we feel most at home since 2016.

Ever since have we remained among their faithful supporters and participants. This gathering of many of our fellow French computer scientists and industrial actors alike has been our go-to conference to catch-up with and present our work. The 2022 edition was no exception!

We submitted and presented the following papers:

• Mikino, formal verification made accessible (link to dedicated blogpost);
• Connecting Software Heritage with the OCaml ecosystem;
• Alt-Ergo-Fuzz, hunting the bugs of the bug hunter;

You can find a more detailed recounting of our JFLA2022 submissions in this blog post as well as the links to the actual (french-written) submitted papers.

Conclusion

As always, we warmly thank all our clients, partners, and friends, for their support and collaboration throughout the year,

And to you, dear reader, thank you for tagging along,

Since 2011 with love,

The OCamlPro Team

---

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.