2017 at OCamlPro

---

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods (Alt-Ergo etc.)

In the World of Blockchains

The Liquidity Language for smart contracts

Work of Alain Mebsout, Fabrice Le Fessant, Çagdas Bozman, Michaël Laporte

OCamlPro develops Liquidity, a high level smart contract language for Tezos. Liquidity is a human-readable language, purely functional, statically-typed, whose syntax is very close to the OCaml syntax. Programs can be compiled to the stack-based language (Michelson) of the Tezos blockchain.

To garner interest and adoption, we developed an online editor called "Try Liquidity". Smart-contract developers can design contracts interactively, directly in the browser, compile them to Michelson, run them and deploy them on the alphanet network of Tezos.

Future plans include a full-fledged web-based IDE for Liquidity. Worth mentioning is a neat feature of Liquidity: decompiling a Michelson program back to its Liquidity version, whether it was generated from Liquidity code or not. In practice, this allows to easily read somewhat obfuscated contracts already deployed on the blockchain.

Tezos and the Tezos ICO

Work of Grégoire Henry, Benjamin Canou, Çagdas Bozman, Alain Mebsout, Michael Laporte, Mohamed Iguernlala, Guillem Rieu, Vincent Bernardoff (for DLS) and at times all the OCamlPro team in animated and joyful brainstorms.

Since 2014, the OCamlPro team had been co-designing the Tezos prototype with Arthur Breitman based on Arthur's White Paper, and had undertaken the implementation of the Tezos node and client. A technical prowess and design achievement we have been proud of. In 2017, we developed the infrastructure for the Tezos ICO (Initial Coin Offering) from the ground up, encompassing the web app (back-end and front-end), the Ethereum and Bitcoin (p2sh) multi-signature contracts, as well as the hardware Ledger based process for transferring funds. The ICO, conducted in collaboration with Arthur, was a resounding success — the equivalent of 230 million dollars (in ETH and BTC) at the time were raised for the Tezos Foundation!

This work was allowed thanks to Arthur Breitman and DLS's funding.

In the World of OCaml

Towards OPAM 2.0, the OCaml Package manager

OPAM was born at Inria/OCamlPro with Frederic, Thomas and Louis, and is still maintained here at OCamlPro. Now thanks to Louis Gesbert's thorough efforts and the OCaml Labs contribution, OPAM 2.0 is coming !

• opam is now compiled with a built-in solver, improving the portability, ease of access and user experience (aspcud no longer a requirement)
• new workflows for developers have been designed, including convenient ways to test and install local sources, more reliable ways to share development setups
• the general system has seen a large number of robustness and expressivity improvements, like extended dependencies
• it also provides better caching, and many hooks enabling, among others, setups with sandboxed builds, binary artifacts caching, or end-to-end package signature verification.

More details: on https://opam.ocaml.org/blog and releases on https://github.com/ocaml/opam/releases

This work is allowed thanks to JaneStreet's funding.

Flambda Compilation

Work of Pierre Chambart, Vincent Laviron

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 JaneStreet's team (Mark, Leo and Xavier) aims at overcoming some of flambda's limitations. This huge refactoring will help make OCaml code more maintainable, improving its theoretical grounds. Internal types are clearer, more concise, and possible control flow transformations are more flexible. Overall a precious outcome for industrial users.

This work is allowed thanks to JaneStreet's funding.

OCaml for ia64-HPUX

In 2017, OCamlPro also worked on porting OCaml on HPUX-ia64. This came from a request of CryptoSense, a French startup working on an OCaml tool to secure cryptographic protocols. OCaml had a port on Linux-ia64, that was deprecated before 4.00.0 and even before, a port on HPUX, but not ia64. So, we expected the easiest part would be to get the bytecode version running, and the hardest part to get access to an HPUX-ia64 computer: it was quite the opposite, HPUX is an awkward system where most tools (shell, make, etc.) have uncommon behaviors, which made even compiling a bytecode version difficult. On the contrary, it was actually easy to get access to a low-power virtual machine of HPUX-ia64 on a monthly basis. Also, we found a few bugs in the former OCaml ia64 backend, mostly caused by the scheduler, since ia64 uses explicit instruction parallelism. Debugging such code was quite a challenge, as instructions were often re-ordered and interleaved. Finally, after a few weeks of work, we got both the bytecode and native code versions running, with only a few limitations.

This work was mandated by CryptoSense.

The style-checker Typerex-lint

Work of Çagdas Bozman, Michael Laporte and Clément Dluzniewski.

In 2017, typerex-lint has been improved and extended. Typerex-lint is a style-checker to analyze the sources of OCaml programs, and can be extended using plugins. It allows to automatically check the conformance of a code base to some coding rules. We added some analysis to look for code that doesn't comply with the recommendations made by the SecurOCaml project members. We also made an interactive web output that provides an easy way to navigate in typerex-lint results.

Build systems and tools

Work of Fabrice Le Fessant

Every year in the OCaml world, a new build tool appears. 2017 was not different, with the rise of jbuild/dune. jbuild came with some very nice features, some of which were already in our home-made build tool, ocp-build, like the ability to build multiple packages at once in a composable way, some other ones were new, like the ability to build multiple versions of the package in one run or the wrapping of libraries using module aliases. We have started to incorporate some of these features in ocp-build. Nevertheless, from our point of view, the two tools belong to two different families: jbuild/dune belongs to the "implicit" family, like ocamlbuild and oasis, with minimal project description; ocp-build belongs to the "explicit" family, like make and omake. We prefer the explicit family, because the build file acts as a description of the project, an entry point to understand the project and the modules. Also, we have kept working on improving the project description language for ocp-build, something that we think is of utmost importance. Latest release: ocp-build 1.99.20-beta.

Other contributions and software

• OCaml bugfixes by Pierre Chambart, Vincent Laviron, and other members of the team.
• The ocp-analyzer prototype by Vincent Laviron

In the World of Formal Methods

Alt-Ergo

By Mohamed Iguernlala

For Alt-Ergo, 2017 was the year of floating-point arithmetic reasoning. Indeed, in addition to the publication of our results at the 29th International Conference on Computer Aided Verification (CAV), Jul 2017, we polished the prototype we started in 2016 and integrated it in the main branch. This is a joint work with Sylvain Conchon (Paris-Saclay University) and Guillaume Melquiond (Inria Lab) in the context of the SOPRANO ANR Project. Another big piece of work in 2017 consisted in investigating a better integration of an efficient CDCL-based SAT solver in Alt-Ergo. In fact, although modern CDCL SAT solvers are very fast, their interaction with the decision procedures and quantifiers instantiation should be finely tuned to get good results in the context of Satisfiability Modulo Theories. This new solver should be integrated into Alt-Ergo in the next few weeks. This work has been done in the context of the LCHIP FUI Project.

We also released a new major version of Alt-Ergo (2.0.0) with a modification in the licensing scheme. Alt-Ergo@OCamlPro's development repository is now made public. This will allow users to get updates and bugfixes as soon as possible.

Towards a formalized type system for OCaml

• Work of Pierrick Couderc, Grégoire Henry, Fabrice Le Fessant and Michel Mauny (Inria Paris)

OCaml is known for its rich type system and strong type inference, unfortunately such complex type engine is prone to errors, and it can be hard to come up with clear idea of how typing works for some features of the language. For 3 years now, OCamlPro has been working on formalizing a subset of this type system and implementing a type checker derived from this formalization. The idea behind this work is to help the compiler developers ensure some form of correctness of the inference. This type checker takes a Typedtree, the intermediate representation resulting from the inference, and checks its consistency. Put differently, this tool checks that each annotated node from the Typedtree can be indeed given such a type according to the context, its form and its sub-expressions. In practice, we could check and catch some known bugs resulting from unsound programs that were accepted by the compiler.

This type checker is only available for OCaml 4.02 for the moment, and the document describing this formalized type system will be available shortly in a PhD thesis, by Pierrick Couderc.

Around the World

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

• The ICFP'2017 (Oxford)
• The JFLA'2017 (Gourette, Pyrénées)
• The CAV'2017 (29th International Conference on Computer Aided Verification, Heidelberg)
• The POSS'2017 (Paris)

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

A few hints about what's ahead for OCamlPro

Let's keep up the good work!

---

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.