Hello Here is the latest OCaml Weekly News, for the week of August 10 to 17, 2021. Table of Contents ───────────────── http-multipart-formdata v3.0.1 released Call for participation: ML Family Workshop 2021 Coq-of-ocaml to translate OCaml to Coq Old CWN http-multipart-formdata v3.0.1 released ═══════════════════════════════════════ Archive: Continuing the thread from last week, Hannes Mehnert asked ────────────────────────────────────────────────────────── 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? [http-multipart-formdata] [multipart_form] [multipart-form-data] Bikal Lem replied ───────────────── 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. Bikal Lem added ─────────────── I should also add `http-multipart-formdata' has been implemented with zero-copy streaming and minimal allocation in mind. Call for participation: ML Family Workshop 2021 ═══════════════════════════════════════════════ Archive: Jonathan Protzenko announced ──────────────────────────── 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: • Keynote: - • ICFP home: Program committee ╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌ • Danel Ahman (University of Ljubljana) • Robert Atkey (University of Strathclyde) • Frédéric Bour (Tarides) • Ezgi Çiçek (Facebook London) • Youyou Cong (Tokyo Institute of Technology) • Richard A. Eisenberg (Tweag I/O) • Martin Elsman (University of Copenhagen, Denmark) • Ohad Kammar (University of Edinburgh) • Naoki Kobayashi (University of Tokyo, Japan) • Benoît Montagu (Inria) • Jonathan Protzenko (Microsoft Research) (Chair) • Kristina Sojakova (INRIA Paris) • Don Syme (Microsoft) • Matías Toro (University of Chile) • Katsuhiro Ueno (Tohoku University) Coq-of-ocaml to translate OCaml to Coq ══════════════════════════════════════ Archive: Guillaume Claret announced ────────────────────────── 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. [coq-of-ocaml] [Coq] [coq-tezos-of-ocaml] [economic protocol] [Tezos] [src/proto_alpha/lib_protocol/script_comparable.ml] [src/Proto_alpha/Proofs/Script_comparable.v] Old CWN ═══════ If you happen to miss a CWN, you can [send me a message] and I'll mail it to you, or go take a look at [the archive] or the [RSS feed of the archives]. If you also wish to receive it every week by mail, you may subscribe [online]. [Alan Schmitt] [send me a message] [the archive] [RSS feed of the archives] [online] [Alan Schmitt]