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
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.
– These new features are described on the new RFC repository for OCaml (a similar idea was suggested and implemented in 2011 by Fabrice Le Fessant).
– The implementation is available on GitHub for both functorized packs and recursive packs. Be aware that both are based on an old version of OCaml for now, but should be in sync with the current trunk in the near future.
– See also Vincent’s OCamlPro’s compiler team work update of August 2019.
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 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
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.
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.
For the record:
– (April 2019) We had started Techelson: a testing framework for Michelson and Liquidity
– (Nov 2018) An Introduction to Tezos RPCs: Signing Operations / An Introduction to Tezos RPCs: a Basic Wallet / Liquidity Tutorial: A Game with an Oracle for Random Numbers / First Open-Source Release of TzScan
– (Oct 2018) OCamlPro’s TZScan grant proposal accepted by the Tezos Foundation – joint press release
– (Jul 2018) OCamlPro’s Tezos block explorer TzScan’s last updates
– (Feb 2018) Release of a first version of TzScan.io, a Tezos block explorer / OCamlPro’s Liquidity-lang demo at JFLA2018 – a smart-contract design language . We were developing Liquidity, a high level smart contract language, human-readable, purely functional, statically-typed, which syntax was very close to the OCaml syntax.
– To garner interest and adoption, we also developed the online editor Try Liquidity. Smart-contract developers could design contracts interactively, directly in the browser, compile them to Michelson, run them and deploy them on the alphanet network of Tezos. Future plans included a full-fledged web-based IDE for Liquidity. Worth mentioning was a neat feature: decompiling a Michelson program back to its Liquidity version, whether it was generated from Liquidity code or not.