Congratulation to the OCaml team for the 2023 SIGPLAN programming languages software award! 🏆

Community
1

Congratulation to the OCaml team for the 2023 SIGPLAN programming languages software award! :trophy:​

https://www.sigplan.org/Awards/Software/

(Just announced at SIGPLAN: Awards Lunch at PLDI23)

IMG_6540
IMG_65401317Ă—736 182 KB

39 Likes
2

IMG_6539
IMG_65391325Ă—747 110 KB

10 Likes
3

To follow up on @spdegabrielle’s nice message: the SIGPLAN PL Software Award 2023 was formally given to the OCaml development team last week at POPL 2024 in London, and I was very pleased and honored to give the reception speech on behalf of the team. For the record, I’ll post the speech next.

6 Likes
4

It’s an honor for the whole OCaml development team to receive such a prestigious award. Some of us are here tonight: Gabriel Scherer, Damien Doligez, Florian Angeletti, Luc Maranget, David Allsopp, Stephen Dolan, Nicolas Ojeda Bär, and I’m Xavier Leroy. It’s two, almost three generations of computer scientists and developers that are being honored…

There is no denying that OCaml has been a long-term project. I released the first version of OCaml, then called Objective Caml, in 1996, almost 28 years ago. But it was already the consolidation of much earlier work, going back more than 50 years from now:

  • Robin Milner’s work on “ML”, the Meta Language (scripting language) of his LCF proof assistant, which introduced the lovely type system and type inference algorithm we all know.

  • Then GĂ©rard Huet brought LCF ML back home to Rocquencourt on a magnetic tape, and liked it so much that with Guy Cousineau and their students, they developed CAML, an implementation of Milner’s ML using the CAM (the Categorical Abstract Machine) as intermediate language – hence the CAML name. And they used it as the implementation language for what was to become the Coq proof assistant.

  • Then, two students of Cousineau at ENS, Damien Doligez and I, fell in love with the CAML language and developed Caml Light, a lightweight, open-source implementation of CAML suitable for teaching and popularizing the language.

So, the 1996 1.0 release of OCaml was already a consolidation of the CAML language, the memory management and virtual machine from Caml Light, my early 1990’s work on native compilation and Standard ML-style module systems, and Jérôme Vouillon’s PhD work on type systems and type inference for objects.

Since then, OCaml has continued to pick up new features arising from PL research, such as Generalized Algebraic Data Types in the late 2000’s, or very recently user-defined effects and effect handlers, making OCaml one of the first non-experimental languages to support effects. This arose from the Multicore OCaml project, along with support for shared-memory parallelism, at long last!, and a new relaxed memory model.

But that’s not the only way in which OCaml has served and continues to serve research in programming languages. If you look at previous recipients for this SIGPLAN software system award, you’ll find the Coq proof assistant, which is implemented in OCaml; the CompCert C compiler, which also uses OCaml for its non-verified parts; as well as WebAssembly, whose reference interpreter is written in OCaml. And looking at possible future recipients, you’ll find Rust, whose first compiler was written in OCaml; STAN, the probabilistic programming language whose compiler was recently rewritten in OCaml; and JSCert, the Javascript formalization that also uses OCaml for its reference interpreter.

Of course, these are not the only uses of OCaml! For something completely different: how many of you took the Eurostar train to come here? or flew an Airbus plane? Chances are that a good chunk of the software embedded in your plane or in your train was generated from SCADE block diagrams by an OCaml program, the SCADE KCG 6 compiler.

So, we’re very proud of our greater user community and all they do with OCaml, both in classic application areas for ML languages such as theorem provers, proof assistants, static analyzers, verification tools, compilers, code generators, etc.; and in more unusual areas such as systems programming.

When Damien and I were hacking Caml Light in 1990, we had no idea that 10 years later the Ensemble people at Cornell and IBM would reimplement a whole network and protocol stack for distributed applications in OCaml and get better latency than their previous C++ implementation. Then came real-time trading, web radios and audio streaming, the Irmin distributed database, Mirage unikernels that boot on a bare hypervisor, and more.

What made that possible? Not just fancy types and nice modules – even though systems programmers value type safety and modularity highly – but also basic properties of OCaml:

  • a language with a simple cost model, where it’s easy to track how much time and how much space is used;
  • a compiler that produces efficient code that looks like the source code, with only predictable optimizations;
  • a low-latency garbage collector, usable for soft real-time applications.
    To us PL folks, this doesn’t sound like much. Good luck getting a paper accepted at POPL or PLDI based on these ideas! Yet, that’s crucial to open the way to many exciting applications.

Will there be other chance encounters with new application areas like this for OCaml in the future? I have no idea – and that’s what makes PL research exciting, even after all these years!

At any rate, we, the recipients of this award, are proud of the achievements of the OCaml user community, and deeply honored to see our efforts recognized by this award. Thank you!

47 Likes