2019 at OCamlPro

Authors: Muriel, OCamlPro
Date: 2020-02-04
Category: OCamlPro
Tags: compiler, cheat sheet, OCamlPro, opam, Rust, Try-OCaml, OCaml, Alt-Ergo, blockchains, Flambda2


2019 at OCamlPro

OCamlPro was created to help OCaml and formal methods spread into the industry. We grew from 1 to 21 engineers, still strongly sharing this ambitious goal! The year 2019 at OCamlPro was very lively, with fantastic accomplishments all along!

Let's quickly review the past years' works, first in the world of OCaml (flambda2 & compiler optimisations, opam 2, our Rust-based UI for memprof, tools like tryOCaml, ocp-indent, and supporting the OCaml Software Foundation), then in the world of formal methods (new versions of our SMT Solver Alt-Ergo, launch of the Alt-Ergo Users' Club, the Love language, etc.).

In the World of OCaml

ocaml

Flambda/Compilation Team

Work by Pierre Chambart, Vincent Laviron, Guillaume Bury and Pierrick Couderc

Pierre and Vincent's considerable work on Flambda 2 (the optimizing intermediate representation of the OCaml compiler – on which inlining occurs), in close cooperation with Jane Street (Mark Shinwell, Leo White and their team) aims at overcoming some of flambda's limitations. We have continued our work on making OCaml programs always faster: internal types are clearer, more concise, and possible control flow transformations are more flexible. Overall a precious outcome for industrial users. In 2019, the major breakthrough was to go from the initial prototype to a complete compiler, which allowed us to compile simple examples first and then to bootstrap it.

On the OCaml compiler side, we also worked with Leo on two new features: functorized compilation units and functorized packs, and recursive packs. The former will allow any developer to implement .ml files as if they were functors and not simply modules, and more importantly generate packs that are real functors. As such, this allows to split big functors into several files or to parameterize libraries on other modules. The latter allows two distinct usages: recursive interfaces, to implement recursive types into distinct .mlis as long as they do not need any implementation; and recursive packs, whose components are typed and compiled as recursive modules.

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

Work on a formalized type system for OCaml

Work of Pierrick Couderc

At the end of 2018, Pierrick defended his PhD on "Checking type inference results of the OCaml language", leading to a formalized type systems and semantics for a large subset of OCaml, or at least its unique typed intermediate language: the Typedtree. This work led us to work on new aspects of the OCaml compiler as recursive and functorized packs described earlier, and we hope this proves useful in the future for the evolution of the language.

The OPAM package manager

Work of Raja Boujbel and Louis Gesbert

opam

OPAM is maintained and developed at OCamlPro by Louis and Raja. Thanks to their thorough efforts the opam 2.1 first release candidate is soon to be published!

Back in 2018, the long-awaited opam 2.0 version was finally released. It embedded many changes, in opam itself as well as for the community. The opam file format was redefined to simplify and add new features. With the close collaboration of OCamlLabs and opam repository maintainers, we were able to manage a smooth transition of the repository and whole ecosystem from opam 1.2 format to the new – and richer – opam 2.0 format. Other emblematic features are e.g. for practically integrated mccs solver, sandboxing builds, for security issues (we care about your filesystem!), for usability reworking of the pin' command, etc.

While the 2.1.0 version is in preparation, the 2.0.0 version is still updated with minor releases to fix issues. The lastest 2.0.6 release is fresh from January.

In the meantime, we continued to improve opam by integrating some opam plugins (opam lock, opam depext), recursively discover opam files in the file tree when pinning, new definition of a switch compiler, the possibility to use z3 backend instead of mccs, etc.

All these new features – among others – will be integrated in the 2.1.0 release, that is betaplanned for February. The best is yet to come!

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

Encouraging OCaml adoption

OCaml Expert trainings for professional programmers

We proposed in 2019 some OCaml expert training specially designed for developers who want to use advanced features and master all the open-source tools and libraries of OCaml.

The "Expert" OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write "compiler-optimizable" code. These sessions are also an opportunity to come discuss with our OPAM & Flambda lead developers and core contributors in Paris.

Next session: 3-4 March 2020, Paris (registration)

Our cheat-sheets on OCaml, the stdlib and opam

Work of Thomas Blanc, Raja Boujbel and Louis Gesbert

Thomas announced the release of our up-to-date cheat-sheets for the OCaml language, standard library and opam. Our original cheat-sheets were dating back to 2011. This was an opportunity to update them after the many changes in the language, library and ecosystem overall.

Cheat-sheets are helpful to refer to, as an overview of the documentation when you are programming, especially when you’re starting in a new language. They are meant to be printed and pinned on your wall, or to be kept in handy on a spare screen. They come in handy when your rubber duck is rubbish at debugging your code!

More details on Thomas' blog post

Open Source Tooling and Web IDEs

And let's not forget the other tools we develop and maintain! We have tools for education such as our interactive editor OCaml-top and Try-OCaml (from the previous work on the learn-OCaml platform for the OCaml Fun MOOC) which you can use to code in your browser. Developers will appreciate tools like our indentation tool ocp-indent, and ocp-index which gives you easy access to the interface information of installed OCaml libraries for editors like Emacs and Vim.

Supporting the OCaml Software Foundation

OCamlPro was proud to be one of the first supporters of the new Inria's OCaml Software Foundation. We keep committed to the adoption of OCaml as an industrial language:

"[…] As a long-standing supporter of the OCaml language, we have always been committed to helping spread OCaml's adoption and increase the accessibility of OCaml to beginners and students. […] We value close and friendly collaboration with the main actors of the OCaml community, and are proud to be contributing to the OCaml language and tooling." (August 2019, Advisory Board of the OCSF, ICFP Berlin)

More information on the OCaml Software Foundation

In the World of Formal Methods

By Mohamed Iguernlala, Albin Coquereau, Guillaume Bury

In 2018, we welcomed five new engineers with a background in formal methods. They consolidate the department of formal methods at OCamlPro, in particular help develop and maintain our SMT solver Alt-Ergo.

Release of Alt-Ergo 2.3.0, and version 2.0.0 (free)

After the release of Alt-Ergo 2.2.0 (with a new front-end that supports the SMT-LIB 2 language, extended prenex polymorphism, implemented as a standalone library) came the version 2.3.0 in 2019 with new features : dune support, ADT / algebraic datatypes, improvement of the if-then-else and let-in support, improvement of the data types.

  • More information on the Alt-Ergo SMT Solver
  • Albin Coquereau defended his PhD thesis in Decembre 2019 "Improving performance of the SMT solver Alt-Ergo with a better integration of efficient SAT solver"
  • We participated in the SMT-COMP 2019 during the 22nd SAT conference. The results of the competition are detailed here.

The launch of the Alt-Ergo Users' Club

Getting closer to our users, gathering industrial and academic supporters, collecting their needs into the Alt-Ergo roadmap is key to Alt-Ergo's development and sustainability.

The Alt-Ergo Users' Club was officially launched beginning of 2019. The first yearly meeting took place in February 2019. We were happy to welcome our first members Adacore, CEA List, Trust-In-Soft, and now Mitsubishi MERCE.

More information on the Alt-Ergo Users' Club

Love-language

Harnessing our language-design expertise: Love

Work by David Declerck & Steven de Oliveira

Following the launch of Dune network, the Love language for smart-contracts was born from the collaboration of OCamlPro and Origin Labs. This new language, whose syntax is inspired from OCaml and Liquidity, is an alternative to the Dune native smart contract language Michelson. Love is based on system-F, a type system requiring no type inference and allowing polymorphism. The language has successfully been integrated on the network and the first smart contracts are being written.

LOVE: a New Smart Contract Language for the Dune Network The Love Smart Contract Language: Introduction & Key Features — Part I

Rust-related activities

The OCaml & Rust combo should be a candidate for any ambitious software project!

  • A Rust-based UI for memprof: we started in 2019 to work in collaboration with the memprof developer team on a Rust based UI for memprof. See Pierre and Albin's exposé at the JFLA2020's "Gardez votre mémoire fraiche avec Memthol" (Pierre Chambart , Albin Coquereau and Jacques-Henri Jourdan)
  • Rust training : Rust borrows heavily from functional programming languages to provide very expressive abstraction mechanisms. Because it is a systems language, these mechanisms are almost always zero-cost. For instance, polymorphic code has no runtime cost compared to a monomorphic version.This concern for efficiency also means that Rust lets developers keep a very high level of control and freedom for optimizations. Rust has no Garbage Collection or any form of runtime memory inspection to decide when to free, allocate or re-use memory. But because manual memory management is almost universally regarded as dangerous, or at least very difficult to maintain, the Rust compiler has a borrow-checker which is responsible for i) proving that the input program is memory-safe (and thread-safe), and ii) generating a safe and “optimal” allocation/deallocation strategy. All of this is done at compile-time.
  • Next sessions: April 20-24th 2020 (registration)

OCamlPro around the world

OCamlPro's team members attended many events throughout the world:

As a committed member of the OCaml ecosystem's animation, we've organized OCaml meetups too (see the famous OUPS meetups in Paris!).

Now let's jump into the new year 2020, with a team keeping expanding, and new projects ahead: keep posted!

Past projects: blockchain-related achievements (2018-beginning of 2019)

Many people ask us about what happened in 2018! That was an incredibly active year on blockchain-related achievements, and at that time we were hoping to attract clients that would be interested in our blockchain expertise.

But that is history now! Still interested? Check the Origin Labs team and their partner The Garage on Dune Network!

For the record:


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.