[Caml-list] Attn: Development Editor, Latest OCaml Weekly News

Alan Schmitt
2021-08-17T06:24:41Z

[-- Attachment #1: Type: text/plain, Size: 9249 bytes --]

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:
<https://discuss.ocaml.org/t/ann-http-multipart-formdata-v3-0-1-released/8261/2>

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]
<https://github.com/lemaetech/http-multipart-formdata>

[multipart_form] <https://github.com/dinosaure/multipart_form/>

[multipart-form-data]
<https://github.com/cryptosense/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:
<https://sympa.inria.fr/sympa/arc/caml-list/2021-08/msg00005.html>

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:
<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>

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:
<https://discuss.ocaml.org/t/coq-of-ocaml-to-translate-ocaml-to-coq/8288/1>

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] <https://clarus.github.io/coq-of-ocaml/>

[Coq] <https://coq.inria.fr/>

[coq-tezos-of-ocaml]
<https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/>

[economic protocol]
<https://gitlab.com/tezos/tezos/-/tree/master/src/proto_alpha/lib_protocol>

[Tezos] <https://tezos.com/>

[src/proto_alpha/lib_protocol/script_comparable.ml]
<https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/script_comparable.ml>

[src/Proto_alpha/Proofs/Script_comparable.v]
<https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_comparable>

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] <mailto:alan.schmitt@polytechnique.org>

[the archive] <https://alan.petitepomme.net/cwn/>

[RSS feed of the archives] <https://alan.petitepomme.net/cwn/cwn.rss>

[online] <http://lists.idyll.org/listinfo/caml-news-weekly/>

[Alan Schmitt] <https://alan.petitepomme.net/>

[-- Attachment #2: Type: text/html, Size: 20527 bytes --]