OCaml Weekly News

Thanks for your work on that. I'm curious about the different "multipart" libraries now available for OCaml – anyone has a brief comparison of them?

• http-multipart-formdata as announced above
• multipart_form by @dinosaure
• multipart-form-data by cryptosense

Are there functional differences? Correctness? Performance? Or just a matter of style and co-development?

One obvious difference among the three is http-multipart-formdata doesn't depend on any IO/Promise libraries, such as lwt or async. so you may find it easier to integrate in your project.

mulitpart-form-data exposes a callback based streaming api, whereas http-multipart-formdata exposes a non-callback, non-blocking based API streaming api.

The API surface of http-multipart-formdata is kept as low as possible, primarily 3 API calls - boundary, reader and read call.

The dependency list of http-multipart-formdata is the thinnest. This may or may not be an issue depending on your aesthetics. However, relatively/comparatively the less your dependencies, the easier it is to integrate the lib with other OCaml libs and environments such as various OSes.

I should also add http-multipart-formdata has been implemented with zero-copy streaming and minimal allocation in mind.

We are happy to announce that the ML Family Workshop is back for its 2021 edition, which we will be held online on Thursday August 26th, in conjunction with ICFP 2021. We invite you to subscribe to, and attend the workshop, in addition to the main ICFP conference.

We are thrilled to announce that Don Syme will give this year's keynote: "Narratives and Lessons from The Early History of F#". Please join us!

The program features 14 exciting submissions, including 4 short talks. The workshop will be held online in the 6pm-3am time band (Seoul Time). Talks will be pre-recorded and uploaded online for those who cannot attend.

• Program: https://icfp21.sigplan.org/home/mlfamilyworkshop-2021#program
• Keynote: https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/15/Keynote-Narratives-and-Lessons-from-The-Early-History-of-F-
• ICFP home: http://icfp21.sigplan.org/home

I am pleased to present the coq-of-ocaml project, to translate a subset of OCaml to the Coq proof assistant. The aim is to do formal verification on OCaml programs. The idea is to generate a Coq translation as close as possible to the original code in terms of intent but using the Coq syntax. As a short example, if we take the following OCaml code and run coq-of-ocaml:

type 'a tree =
| Leaf of 'a
| Node of 'a tree * 'a tree

let rec sum tree =
  match tree with
  | Leaf n -> n
  | Node (tree1, tree2) -> sum tree1 + sum tree2

we get the following Coq file:

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Inductive tree (a : Set) : Set :=
| Leaf : a -> tree a
| Node : tree a -> tree a -> tree a.

Arguments Leaf {_}.
Arguments Node {_}.

Fixpoint sum (tree : tree int) : int :=
  match tree with
  | Leaf n => n
  | Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
  end.

We support the following OCaml features:

• the core of OCaml (functions, let bindings, pattern-matching,…)
• type definitions (records, inductive types, synonyms, mutual types)
• monadic programs
• modules as namespaces
• modules as polymorphic records (signatures, functors, first-class modules)
• multiple-file projects (thanks to Merlin)
• both .ml and .mli files
• existential types (we use impredicative sets option in Coq)

We also have some support for the GADTs, the polymorphic variants, and the extensible types. We are in particular working on having an axiom-free translation of the GADTs to Coq. We do not support:

• side-effects outside of a monad (references, exceptions, …);
• object-oriented programming;
• various combinations of OCaml features for which coq-of-ocaml should generate a warning.

Our main example and use case is the coq-tezos-of-ocaml project. This contains a translation of most of the economic protocol of the Tezos blockchain (around 30.000 lines of OCaml translated to 40.000 lines of Coq). For example, we verify the comparison functions defined in src/proto_alpha/lib_protocol/script_comparable.ml with src/Proto_alpha/Proofs/Script_comparable.v.

We are looking for the application to other projects too.

We think the best way to use coq-of-ocaml is to continue developing in OCaml and run coq-of-ocaml to keep a synchronized translation in Coq. Having a working Coq translation (as compiling in Coq) forces us to avoid some OCaml constructs. We believe these constructs would probably be hard to verify anyway. Then, on the Coq side, we can verify some important or easy to catch properties. If there is a regression in the OCaml code, re-running coq-of-ocaml should make the proofs break.